MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp43 Structured version   Visualization version   GIF version

Theorem exp43 639
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp43.1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
exp43 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp43
StepHypRef Expression
1 exp43.1 . . 3 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
21ex 450 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 631 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  exp53  646  funssres  5918  fvopab3ig  6265  fvmptt  6286  fvn0elsuppb  7297  tfr3  7480  omordi  7631  odi  7644  nnmordi  7696  php  8129  fiint  8222  ordiso2  8405  cfcoflem  9079  zorn2lem5  9307  inar1  9582  psslinpr  9838  recexsrlem  9909  qaddcl  11789  qmulcl  11791  elfznelfzo  12557  expcan  12896  ltexp2  12897  bernneq  12973  expnbnd  12976  relexpaddg  13774  lcmfunsnlem2lem1  15332  initoeu2lem1  16645  elcls3  20868  opnneissb  20899  txbas  21351  grpoidinvlem3  27330  grporcan  27342  shscli  28146  spansncol  28397  spanunsni  28408  spansncvi  28481  homco1  28630  homulass  28631  atomli  29211  chirredlem1  29219  cdj1i  29262  frinfm  33501  filbcmb  33506  unichnidl  33801  dmncan1  33846  pclfinclN  35055  iccelpart  41133  prmdvdsfmtnof1lem2  41262  scmsuppss  41918
  Copyright terms: Public domain W3C validator