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

Theorem exp43 437
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 413 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 431 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  exp53  448  funssres  6543  fvopab3ig  6942  fvmptt  6966  fvn0elsuppb  8109  tfr3  8342  omordi  8510  odi  8523  nnmordi  8575  php  9151  phpOLD  9163  fiint  9265  ordiso2  9448  cfcoflem  10205  zorn2lem5  10433  inar1  10708  psslinpr  10964  recexsrlem  11036  qaddcl  12887  qmulcl  12889  elfznelfzo  13674  expcan  14071  ltexp2  14072  bernneq  14129  expnbnd  14132  relexpaddg  14935  lcmfunsnlem2lem1  16511  initoeu2lem1  17897  elcls3  22430  opnneissb  22461  txbas  22914  grpoidinvlem3  29346  grporcan  29358  shscli  30157  spansncol  30408  spanunsni  30419  spansncvi  30492  homco1  30641  homulass  30642  atomli  31222  chirredlem1  31230  cdj1i  31273  satffunlem  33886  frinfm  36183  filbcmb  36188  unichnidl  36479  dmncan1  36524  pclfinclN  38402  iccelpart  45595  prmdvdsfmtnof1lem2  45747  scmsuppss  46418  iscnrm3lem4  46939
  Copyright terms: Public domain W3C validator