Theorem 3exp 1138

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

Syntax hints:   → wi 4   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3expa  1139  3expb  1140  3expia  1141  3expib  1142  3com23  1145  3an1rs  1151  3exp1  1155  3expd  1156  exp5o  1158  syl3an2  1204  syl3an3  1205  syl2an23an  1231  3impexpbicomi  1369  rexlimdv3a  2484  rabssdv  3083  reupick2  3266  ssorduni  4259  tfisi  4356  fvssunirng  5241  f1oiso2  5517  poxp  5904  tfrlem5  5983  nndi  6150  nnmass  6151  findcard  6444  ac6sfi  6454  mulcanpig  6639  divgt0  8069  divge0  8070  uzind  8591  uzind2  8592  facavg  9822  dvdsnprmd  10714  prmndvdsfaclt  10742