Theorem 3exp 1229

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3expa  1230  3expb  1231  3expia  1232  3expib  1233  3com23  1236  3an1rs  1246  3exp1  1250  3expd  1251  exp5o  1253  syl3an2  1308  syl3an3  1309  syl2an23an  1336  3impexpbicomi  1485  rexlimdv3a  2662  rabssdv  3318  reupick2  3507  ssorduni  4609  tfisi  4709  fvssunirng  5685  f1oiso2  6000  poxp  6428  tfrlem5  6545  nndi  6719  nnmass  6720  findcard  7145  ac6sfi  7155  mulcanpig  7650  divgt0  9146  divge0  9147  uzind  9689  uzind2  9690  facavg  11108  prodfap0  12231  prodfrecap  12232  fprodabs  12302  dvdsmodexp  12481  dvdsaddre2b  12527  dvdsnprmd  12822  prmndvdsfaclt  12853  fermltl  12931  pceu  12993  mulgass2  14202  islss4  14530  rnglidlmcl  14628  fiinopn  14869  neipsm  15019  tpnei  15025  opnneiid  15029  neibl  15356  tgqioo  15420  gausslemma2dlem1a  15931  ausgrumgrien  16165  ausgrusgrien  16166  usgrausgrben  16167  ushgredgedg  16221  ushgredgedgloop  16223  wlkl1loop  16353