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

Theorem 3exp 1197
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 1171 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 71 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 973
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 975
This theorem is referenced by:  3expa  1198  3expb  1199  3expia  1200  3expib  1201  3com23  1204  3an1rs  1214  3exp1  1218  3expd  1219  exp5o  1221  syl3an2  1267  syl3an3  1268  syl2an23an  1294  3impexpbicomi  1432  rexlimdv3a  2589  rabssdv  3227  reupick2  3413  ssorduni  4471  tfisi  4571  fvssunirng  5511  f1oiso2  5806  poxp  6211  tfrlem5  6293  nndi  6465  nnmass  6466  findcard  6866  ac6sfi  6876  mulcanpig  7297  divgt0  8788  divge0  8789  uzind  9323  uzind2  9324  facavg  10680  prodfap0  11508  prodfrecap  11509  fprodabs  11579  dvdsmodexp  11757  dvdsnprmd  12079  prmndvdsfaclt  12110  fermltl  12188  pceu  12249  fiinopn  12796  neipsm  12948  tpnei  12954  opnneiid  12958  neibl  13285  tgqioo  13341
  Copyright terms: Public domain W3C validator