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

Theorem exp43 440
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 416 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 434 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  exp53  451  funssres  6368  fvopab3ig  6741  fvmptt  6765  fvn0elsuppb  7830  tfr3  8018  omordi  8175  odi  8188  nnmordi  8240  php  8685  fiint  8779  ordiso2  8963  cfcoflem  9683  zorn2lem5  9911  inar1  10186  psslinpr  10442  recexsrlem  10514  qaddcl  12352  qmulcl  12354  elfznelfzo  13137  expcan  13529  ltexp2  13530  bernneq  13586  expnbnd  13589  relexpaddg  14404  lcmfunsnlem2lem1  15972  initoeu2lem1  17266  elcls3  21688  opnneissb  21719  txbas  22172  grpoidinvlem3  28289  grporcan  28301  shscli  29100  spansncol  29351  spanunsni  29362  spansncvi  29435  homco1  29584  homulass  29585  atomli  30165  chirredlem1  30173  cdj1i  30216  satffunlem  32761  frinfm  35173  filbcmb  35178  unichnidl  35469  dmncan1  35514  pclfinclN  37246  iccelpart  43948  prmdvdsfmtnof1lem2  44100  scmsuppss  44772
  Copyright terms: Public domain W3C validator