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

Theorem 3exp 1103
 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 1083 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 65 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  3expa  1104  3expb  1105  3expia  1106  3expib  1107  3com23  1110  3an1rs  1116  3exp1  1120  3expd  1121  exp5o  1123  syl3an2  1169  syl3an3  1170  3impexpbicomi  1328  rexlimdv3a  2435  rabssdv  3020  reupick2  3223  ssorduni  4213  tfisi  4310  fvssunirng  5190  f1oiso2  5466  poxp  5853  tfrlem5  5930  nndi  6065  nnmass  6066  findcard  6345  ac6sfi  6352  mulcanpig  6433  divgt0  7838  divge0  7839  uzind  8349  uzind2  8350
 Copyright terms: Public domain W3C validator