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  4636  tfisi  4736  fvssunirng  5713  f1oiso2  6036  poxp  6472  tfrlem5  6590  nndi  6764  nnmass  6765  findcard  7198  ac6sfi  7208  mulcanpig  7708  divgt0  9210  divge0  9211  uzind  9767  uzind2  9768  facavg  11205  prodfap0  12336  prodfrecap  12337  fprodabs  12407  dvdsmodexp  12586  dvdsaddre2b  12632  dvdsnprmd  12927  prmndvdsfaclt  12959  fermltl  13040  pceu  13102  mulgass2  14469  islss4  14827  rnglidlmcl  14925  fiinopn  15247  neipsm  15397  tpnei  15403  opnneiid  15407  neibl  15734  tgqioo  15798  bcmono  16321  gausslemma2dlem1a  16399  ausgrumgrien  16633  ausgrusgrien  16634  usgrausgrben  16635  ushgredgedg  16689  ushgredgedgloop  16691  wlkl1loop  16821