Theorem 3exp 1114

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

Syntax hints:   → wi 4   ∧ w3a 896

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  3expa  1115  3expb  1116  3expia  1117  3expib  1118  3com23  1121  3an1rs  1127  3exp1  1131  3expd  1132  exp5o  1134  syl3an2  1180  syl3an3  1181  3impexpbicomi  1344  rexlimdv3a  2452  rabssdv  3047  reupick2  3250  ssorduni  4240  tfisi  4337  fvssunirng  5217  f1oiso2  5493  poxp  5880  tfrlem5  5960  nndi  6095  nnmass  6096  findcard  6375  ac6sfi  6382  mulcanpig  6490  divgt0  7912  divge0  7913  uzind  8407  uzind2  8408  facavg  9607