Theorem 3exp 1229

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3expa  1230  3expb  1231  3expia  1232  3expib  1233  3com23  1236  3an1rs  1246  3exp1  1250  3expd  1251  exp5o  1253  syl3an2  1308  syl3an3  1309  syl2an23an  1336  3impexpbicomi  1485  rexlimdv3a  2653  rabssdv  3308  reupick2  3495  ssorduni  4591  tfisi  4691  fvssunirng  5663  f1oiso2  5978  poxp  6406  tfrlem5  6523  nndi  6697  nnmass  6698  findcard  7120  ac6sfi  7130  mulcanpig  7598  divgt0  9094  divge0  9095  uzind  9635  uzind2  9636  facavg  11054  prodfap0  12169  prodfrecap  12170  fprodabs  12240  dvdsmodexp  12419  dvdsaddre2b  12465  dvdsnprmd  12760  prmndvdsfaclt  12791  fermltl  12869  pceu  12931  mulgass2  14135  islss4  14461  rnglidlmcl  14559  fiinopn  14798  neipsm  14948  tpnei  14954  opnneiid  14958  neibl  15285  tgqioo  15349  gausslemma2dlem1a  15860  ausgrumgrien  16094  ausgrusgrien  16095  usgrausgrben  16096  ushgredgedg  16150  ushgredgedgloop  16152  wlkl1loop  16282