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

Theorem exp43 637
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 448 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 629 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  exp53  644  funssres  5830  fvopab3ig  6173  fvmptt  6193  fvn0elsuppb  7176  tfr3  7359  omordi  7510  odi  7523  nnmordi  7575  php  8006  fiint  8099  ordiso2  8280  cfcoflem  8954  zorn2lem5  9182  inar1  9453  psslinpr  9709  recexsrlem  9780  qaddcl  11636  qmulcl  11638  elfznelfzo  12394  expcan  12730  ltexp2  12731  bernneq  12807  expnbnd  12810  relexpaddg  13587  lcmfunsnlem2lem1  15135  initoeu2lem1  16433  elcls3  20639  opnneissb  20670  txbas  21122  grpoidinvlem3  26510  grporcan  26522  shscli  27366  spansncol  27617  spanunsni  27628  spansncvi  27701  homco1  27850  homulass  27851  atomli  28431  chirredlem1  28439  cdj1i  28482  frinfm  32503  filbcmb  32508  unichnidl  32803  dmncan1  32848  pclfinclN  34057  iccelpart  39776  prmdvdsfmtnof1lem2  39840  scmsuppss  41949
  Copyright terms: Public domain W3C validator