Theorem 3exp 1181

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

Syntax hints:   → wi 4   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3expa  1182  3expb  1183  3expia  1184  3expib  1185  3com23  1188  3an1rs  1198  3exp1  1202  3expd  1203  exp5o  1205  syl3an2  1251  syl3an3  1252  syl2an23an  1278  3impexpbicomi  1416  rexlimdv3a  2554  rabssdv  3182  reupick2  3367  ssorduni  4411  tfisi  4509  fvssunirng  5444  f1oiso2  5736  poxp  6137  tfrlem5  6219  nndi  6390  nnmass  6391  findcard  6790  ac6sfi  6800  mulcanpig  7167  divgt0  8654  divge0  8655  uzind  9186  uzind2  9187  facavg  10524  prodfap0  11346  prodfrecap  11347  dvdsnprmd  11842  prmndvdsfaclt  11870  fiinopn  12210  neipsm  12362  tpnei  12368  opnneiid  12372  neibl  12699  tgqioo  12755