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

Theorem 3exp 1165
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 1145 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 71 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  3expa  1166  3expb  1167  3expia  1168  3expib  1169  3com23  1172  3an1rs  1182  3exp1  1186  3expd  1187  exp5o  1189  syl3an2  1235  syl3an3  1236  syl2an23an  1262  3impexpbicomi  1400  rexlimdv3a  2528  rabssdv  3147  reupick2  3332  ssorduni  4373  tfisi  4471  fvssunirng  5404  f1oiso2  5696  poxp  6097  tfrlem5  6179  nndi  6350  nnmass  6351  findcard  6750  ac6sfi  6760  mulcanpig  7111  divgt0  8598  divge0  8599  uzind  9130  uzind2  9131  facavg  10460  dvdsnprmd  11733  prmndvdsfaclt  11761  fiinopn  12098  neipsm  12250  tpnei  12256  opnneiid  12260  neibl  12587  tgqioo  12643
  Copyright terms: Public domain W3C validator