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

Theorem exp43 425
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 399 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 419 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 198  df-an 385
This theorem is referenced by:  exp53  436  funssres  6141  fvopab3ig  6496  fvmptt  6518  fvn0elsuppb  7543  tfr3  7728  omordi  7880  odi  7893  nnmordi  7945  php  8380  fiint  8473  ordiso2  8656  cfcoflem  9376  zorn2lem5  9604  inar1  9879  psslinpr  10135  recexsrlem  10206  qaddcl  12019  qmulcl  12021  elfznelfzo  12793  expcan  13132  ltexp2  13133  bernneq  13209  expnbnd  13212  relexpaddg  14012  lcmfunsnlem2lem1  15566  initoeu2lem1  16864  elcls3  21097  opnneissb  21128  txbas  21580  grpoidinvlem3  27685  grporcan  27697  shscli  28501  spansncol  28752  spanunsni  28763  spansncvi  28836  homco1  28985  homulass  28986  atomli  29566  chirredlem1  29574  cdj1i  29617  frinfm  33839  filbcmb  33844  unichnidl  34138  dmncan1  34183  pclfinclN  35727  iccelpart  41941  prmdvdsfmtnof1lem2  42069  scmsuppss  42718
  Copyright terms: Public domain W3C validator