Theorem 3exp 1204

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3expa  1205  3expb  1206  3expia  1207  3expib  1208  3com23  1211  3an1rs  1221  3exp1  1225  3expd  1226  exp5o  1228  syl3an2  1283  syl3an3  1284  syl2an23an  1310  3impexpbicomi  1450  rexlimdv3a  2616  rabssdv  3264  reupick2  3450  ssorduni  4524  tfisi  4624  fvssunirng  5576  f1oiso2  5877  poxp  6299  tfrlem5  6381  nndi  6553  nnmass  6554  findcard  6958  ac6sfi  6968  mulcanpig  7421  divgt0  8918  divge0  8919  uzind  9456  uzind2  9457  facavg  10857  prodfap0  11729  prodfrecap  11730  fprodabs  11800  dvdsmodexp  11979  dvdsaddre2b  12025  dvdsnprmd  12320  prmndvdsfaclt  12351  fermltl  12429  pceu  12491  mulgass2  13692  islss4  14016  rnglidlmcl  14114  fiinopn  14348  neipsm  14498  tpnei  14504  opnneiid  14508  neibl  14835  tgqioo  14899  gausslemma2dlem1a  15407