Theorem 3exp 1203

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 1177	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒))))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl8 71	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 979

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 981

This theorem is referenced by:  3expa  1204  3expb  1205  3expia  1206  3expib  1207  3com23  1210  3an1rs  1220  3exp1  1224  3expd  1225  exp5o  1227  syl3an2  1282  syl3an3  1283  syl2an23an  1309  3impexpbicomi  1449  rexlimdv3a  2606  rabssdv  3247  reupick2  3433  ssorduni  4498  tfisi  4598  fvssunirng  5542  f1oiso2  5841  poxp  6247  tfrlem5  6329  nndi  6501  nnmass  6502  findcard  6902  ac6sfi  6912  mulcanpig  7348  divgt0  8843  divge0  8844  uzind  9378  uzind2  9379  facavg  10740  prodfap0  11567  prodfrecap  11568  fprodabs  11638  dvdsmodexp  11816  dvdsaddre2b  11862  dvdsnprmd  12139  prmndvdsfaclt  12170  fermltl  12248  pceu  12309  mulgass2  13365  islss4  13628  rnglidlmcl  13726  fiinopn  13857  neipsm  14007  tpnei  14013  opnneiid  14017  neibl  14344  tgqioo  14400