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

Theorem 3exp 1140
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 1120 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 70 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 922
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 924
This theorem is referenced by:  3expa  1141  3expb  1142  3expia  1143  3expib  1144  3com23  1147  3an1rs  1153  3exp1  1157  3expd  1158  exp5o  1160  syl3an2  1206  syl3an3  1207  syl2an23an  1233  3impexpbicomi  1371  rexlimdv3a  2487  rabssdv  3090  reupick2  3274  ssorduni  4279  tfisi  4377  fvssunirng  5285  f1oiso2  5569  poxp  5956  tfrlem5  6035  nndi  6203  nnmass  6204  findcard  6558  ac6sfi  6568  mulcanpig  6841  divgt0  8271  divge0  8272  uzind  8793  uzind2  8794  facavg  10054  dvdsnprmd  11013  prmndvdsfaclt  11041
  Copyright terms: Public domain W3C validator