Theorem 3exp 1228

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  3expa  1229  3expb  1230  3expia  1231  3expib  1232  3com23  1235  3an1rs  1245  3exp1  1249  3expd  1250  exp5o  1252  syl3an2  1307  syl3an3  1308  syl2an23an  1335  3impexpbicomi  1484  rexlimdv3a  2652  rabssdv  3307  reupick2  3493  ssorduni  4585  tfisi  4685  fvssunirng  5654  f1oiso2  5968  poxp  6397  tfrlem5  6480  nndi  6654  nnmass  6655  findcard  7077  ac6sfi  7087  mulcanpig  7555  divgt0  9052  divge0  9053  uzind  9591  uzind2  9592  facavg  11009  prodfap0  12124  prodfrecap  12125  fprodabs  12195  dvdsmodexp  12374  dvdsaddre2b  12420  dvdsnprmd  12715  prmndvdsfaclt  12746  fermltl  12824  pceu  12886  mulgass2  14090  islss4  14415  rnglidlmcl  14513  fiinopn  14747  neipsm  14897  tpnei  14903  opnneiid  14907  neibl  15234  tgqioo  15298  gausslemma2dlem1a  15806  ausgrumgrien  16040  ausgrusgrien  16041  usgrausgrben  16042  ushgredgedg  16096  ushgredgedgloop  16098  wlkl1loop  16228