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  3305  reupick2  3491  ssorduni  4583  tfisi  4683  fvssunirng  5650  f1oiso2  5963  poxp  6392  tfrlem5  6475  nndi  6649  nnmass  6650  findcard  7070  ac6sfi  7080  mulcanpig  7545  divgt0  9042  divge0  9043  uzind  9581  uzind2  9582  facavg  10998  prodfap0  12096  prodfrecap  12097  fprodabs  12167  dvdsmodexp  12346  dvdsaddre2b  12392  dvdsnprmd  12687  prmndvdsfaclt  12718  fermltl  12796  pceu  12858  mulgass2  14061  islss4  14386  rnglidlmcl  14484  fiinopn  14718  neipsm  14868  tpnei  14874  opnneiid  14878  neibl  15205  tgqioo  15269  gausslemma2dlem1a  15777  ausgrumgrien  16009  ausgrusgrien  16010  usgrausgrben  16011  ushgredgedg  16065  ushgredgedgloop  16067  wlkl1loop  16155