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

Theorem exp43 641
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 449 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 633 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  exp53  648  funssres  6091  fvopab3ig  6440  fvmptt  6462  fvn0elsuppb  7480  tfr3  7664  omordi  7815  odi  7828  nnmordi  7880  php  8309  fiint  8402  ordiso2  8585  cfcoflem  9286  zorn2lem5  9514  inar1  9789  psslinpr  10045  recexsrlem  10116  qaddcl  11997  qmulcl  11999  elfznelfzo  12767  expcan  13107  ltexp2  13108  bernneq  13184  expnbnd  13187  relexpaddg  13992  lcmfunsnlem2lem1  15553  initoeu2lem1  16865  elcls3  21089  opnneissb  21120  txbas  21572  grpoidinvlem3  27669  grporcan  27681  shscli  28485  spansncol  28736  spanunsni  28747  spansncvi  28820  homco1  28969  homulass  28970  atomli  29550  chirredlem1  29558  cdj1i  29601  frinfm  33843  filbcmb  33848  unichnidl  34143  dmncan1  34188  pclfinclN  35739  iccelpart  41879  prmdvdsfmtnof1lem2  42007  scmsuppss  42663
  Copyright terms: Public domain W3C validator