Theorem 3exp 1228

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  3expa  1229  3expb  1230  3expia  1231  3expib  1232  3com23  1235  3an1rs  1245  3exp1  1249  3expd  1250  exp5o  1252  syl3an2  1307  syl3an3  1308  syl2an23an  1335  3impexpbicomi  1484  rexlimdv3a  2652  rabssdv  3307  reupick2  3493  ssorduni  4585  tfisi  4685  fvssunirng  5654  f1oiso2  5967  poxp  6396  tfrlem5  6479  nndi  6653  nnmass  6654  findcard  7076  ac6sfi  7086  mulcanpig  7554  divgt0  9051  divge0  9052  uzind  9590  uzind2  9591  facavg  11007  prodfap0  12105  prodfrecap  12106  fprodabs  12176  dvdsmodexp  12355  dvdsaddre2b  12401  dvdsnprmd  12696  prmndvdsfaclt  12727  fermltl  12805  pceu  12867  mulgass2  14070  islss4  14395  rnglidlmcl  14493  fiinopn  14727  neipsm  14877  tpnei  14883  opnneiid  14887  neibl  15214  tgqioo  15278  gausslemma2dlem1a  15786  ausgrumgrien  16020  ausgrusgrien  16021  usgrausgrben  16022  ushgredgedg  16076  ushgredgedgloop  16078  wlkl1loop  16208