Theorem 3exp 1205

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  3expa  1206  3expb  1207  3expia  1208  3expib  1209  3com23  1212  3an1rs  1222  3exp1  1226  3expd  1227  exp5o  1229  syl3an2  1284  syl3an3  1285  syl2an23an  1312  3impexpbicomi  1460  rexlimdv3a  2626  rabssdv  3277  reupick2  3463  ssorduni  4543  tfisi  4643  fvssunirng  5604  f1oiso2  5909  poxp  6331  tfrlem5  6413  nndi  6585  nnmass  6586  findcard  7000  ac6sfi  7010  mulcanpig  7468  divgt0  8965  divge0  8966  uzind  9504  uzind2  9505  facavg  10913  prodfap0  11931  prodfrecap  11932  fprodabs  12002  dvdsmodexp  12181  dvdsaddre2b  12227  dvdsnprmd  12522  prmndvdsfaclt  12553  fermltl  12631  pceu  12693  mulgass2  13895  islss4  14219  rnglidlmcl  14317  fiinopn  14551  neipsm  14701  tpnei  14707  opnneiid  14711  neibl  15038  tgqioo  15102  gausslemma2dlem1a  15610