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  4578  tfisi  4678  fvssunirng  5641  f1oiso2  5950  poxp  6376  tfrlem5  6458  nndi  6630  nnmass  6631  findcard  7046  ac6sfi  7056  mulcanpig  7518  divgt0  9015  divge0  9016  uzind  9554  uzind2  9555  facavg  10963  prodfap0  12051  prodfrecap  12052  fprodabs  12122  dvdsmodexp  12301  dvdsaddre2b  12347  dvdsnprmd  12642  prmndvdsfaclt  12673  fermltl  12751  pceu  12813  mulgass2  14016  islss4  14340  rnglidlmcl  14438  fiinopn  14672  neipsm  14822  tpnei  14828  opnneiid  14832  neibl  15159  tgqioo  15223  gausslemma2dlem1a  15731  ausgrumgrien  15962  ausgrusgrien  15963  usgrausgrben  15964  ushgredgedg  16018  ushgredgedgloop  16020