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  12111  prodfrecap  12112  fprodabs  12182  dvdsmodexp  12361  dvdsaddre2b  12407  dvdsnprmd  12702  prmndvdsfaclt  12733  fermltl  12811  pceu  12873  mulgass2  14077  islss4  14402  rnglidlmcl  14500  fiinopn  14734  neipsm  14884  tpnei  14890  opnneiid  14894  neibl  15221  tgqioo  15285  gausslemma2dlem1a  15793  ausgrumgrien  16027  ausgrusgrien  16028  usgrausgrben  16029  ushgredgedg  16083  ushgredgedgloop  16085  wlkl1loop  16215