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

Theorem 3exp 1114
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 1094 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 69 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3expa  1115  3expb  1116  3expia  1117  3expib  1118  3com23  1121  3an1rs  1127  3exp1  1131  3expd  1132  exp5o  1134  syl3an2  1180  syl3an3  1181  3impexpbicomi  1344  rexlimdv3a  2452  rabssdv  3047  reupick2  3250  ssorduni  4240  tfisi  4337  fvssunirng  5217  f1oiso2  5493  poxp  5880  tfrlem5  5960  nndi  6095  nnmass  6096  findcard  6375  ac6sfi  6382  mulcanpig  6490  divgt0  7912  divge0  7913  uzind  8407  uzind2  8408  facavg  9607
  Copyright terms: Public domain W3C validator