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

Theorem 3exp 1163
 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 1143 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 71 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 945 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 947 This theorem is referenced by:  3expa  1164  3expb  1165  3expia  1166  3expib  1167  3com23  1170  3an1rs  1180  3exp1  1184  3expd  1185  exp5o  1187  syl3an2  1233  syl3an3  1234  syl2an23an  1260  3impexpbicomi  1398  rexlimdv3a  2526  rabssdv  3145  reupick2  3330  ssorduni  4371  tfisi  4469  fvssunirng  5402  f1oiso2  5694  poxp  6095  tfrlem5  6177  nndi  6348  nnmass  6349  findcard  6748  ac6sfi  6758  mulcanpig  7107  divgt0  8590  divge0  8591  uzind  9116  uzind2  9117  facavg  10443  dvdsnprmd  11713  prmndvdsfaclt  11741  fiinopn  12077  neipsm  12229  tpnei  12235  opnneiid  12239  neibl  12566  tgqioo  12622
 Copyright terms: Public domain W3C validator