Theorem 3exp 1233

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3expa  1234  3expb  1235  3expia  1236  3expib  1237  3com23  1240  3an1rs  1250  3exp1  1254  3expd  1255  exp5o  1257  syl3an2  1312  syl3an3  1313  syl2an23an  1340  3impexpbicomi  1489  rexlimdv3a  2670  rabssdv  3328  reupick2  3519  ssorduni  4634  tfisi  4734  fvssunirng  5710  f1oiso2  6033  poxp  6468  tfrlem5  6585  nndi  6759  nnmass  6760  findcard  7192  ac6sfi  7202  mulcanpig  7703  divgt0  9205  divge0  9206  uzind  9762  uzind2  9763  facavg  11200  prodfap0  12331  prodfrecap  12332  fprodabs  12402  dvdsmodexp  12581  dvdsaddre2b  12627  dvdsnprmd  12922  prmndvdsfaclt  12954  fermltl  13035  pceu  13097  mulgass2  14447  islss4  14803  rnglidlmcl  14901  fiinopn  15196  neipsm  15346  tpnei  15352  opnneiid  15356  neibl  15683  tgqioo  15747  bcmono  16265  gausslemma2dlem1a  16343  ausgrumgrien  16577  ausgrusgrien  16578  usgrausgrben  16579  ushgredgedg  16633  ushgredgedgloop  16635  wlkl1loop  16765