Theorem 3exp 1226

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3expa  1227  3expb  1228  3expia  1229  3expib  1230  3com23  1233  3an1rs  1243  3exp1  1247  3expd  1248  exp5o  1250  syl3an2  1305  syl3an3  1306  syl2an23an  1333  3impexpbicomi  1482  rexlimdv3a  2650  rabssdv  3304  reupick2  3490  ssorduni  4579  tfisi  4679  fvssunirng  5644  f1oiso2  5957  poxp  6384  tfrlem5  6466  nndi  6640  nnmass  6641  findcard  7058  ac6sfi  7068  mulcanpig  7530  divgt0  9027  divge0  9028  uzind  9566  uzind2  9567  facavg  10976  prodfap0  12064  prodfrecap  12065  fprodabs  12135  dvdsmodexp  12314  dvdsaddre2b  12360  dvdsnprmd  12655  prmndvdsfaclt  12686  fermltl  12764  pceu  12826  mulgass2  14029  islss4  14354  rnglidlmcl  14452  fiinopn  14686  neipsm  14836  tpnei  14842  opnneiid  14846  neibl  15173  tgqioo  15237  gausslemma2dlem1a  15745  ausgrumgrien  15976  ausgrusgrien  15977  usgrausgrben  15978  ushgredgedg  16032  ushgredgedgloop  16034  wlkl1loop  16079