Theorem 3exp 1202

Description: Exportation inference. (Contributed by NM, 30-May-1994.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3exp	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		pm3.2an3 1176	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒))))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl8 71	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3expa  1203  3expb  1204  3expia  1205  3expib  1206  3com23  1209  3an1rs  1219  3exp1  1223  3expd  1224  exp5o  1226  syl3an2  1272  syl3an3  1273  syl2an23an  1299  3impexpbicomi  1439  rexlimdv3a  2596  rabssdv  3235  reupick2  3421  ssorduni  4484  tfisi  4584  fvssunirng  5527  f1oiso2  5823  poxp  6228  tfrlem5  6310  nndi  6482  nnmass  6483  findcard  6883  ac6sfi  6893  mulcanpig  7329  divgt0  8823  divge0  8824  uzind  9358  uzind2  9359  facavg  10717  prodfap0  11544  prodfrecap  11545  fprodabs  11615  dvdsmodexp  11793  dvdsnprmd  12115  prmndvdsfaclt  12146  fermltl  12224  pceu  12285  mulgass2  13135  fiinopn  13284  neipsm  13436  tpnei  13442  opnneiid  13446  neibl  13773  tgqioo  13829