Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3exp GIF version

Theorem 3exp 1138
 Description: Exportation inference. (Contributed by NM, 30-May-1994.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3exp (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem 3exp
StepHypRef Expression
1 pm3.2an3 1118 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 70 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 920 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115  df-3an 922 This theorem is referenced by:  3expa  1139  3expb  1140  3expia  1141  3expib  1142  3com23  1145  3an1rs  1151  3exp1  1155  3expd  1156  exp5o  1158  syl3an2  1204  syl3an3  1205  syl2an23an  1231  3impexpbicomi  1369  rexlimdv3a  2484  rabssdv  3083  reupick2  3266  ssorduni  4259  tfisi  4356  fvssunirng  5241  f1oiso2  5517  poxp  5904  tfrlem5  5983  nndi  6150  nnmass  6151  findcard  6444  ac6sfi  6454  mulcanpig  6639  divgt0  8069  divge0  8070  uzind  8591  uzind2  8592  facavg  9822  dvdsnprmd  10714  prmndvdsfaclt  10742
 Copyright terms: Public domain W3C validator