Theorem 3exp 1180

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

Syntax hints:   → wi 4   ∧ w3a 962

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 964

This theorem is referenced by:  3expa  1181  3expb  1182  3expia  1183  3expib  1184  3com23  1187  3an1rs  1197  3exp1  1201  3expd  1202  exp5o  1204  syl3an2  1250  syl3an3  1251  syl2an23an  1277  3impexpbicomi  1415  rexlimdv3a  2551  rabssdv  3177  reupick2  3362  ssorduni  4403  tfisi  4501  fvssunirng  5436  f1oiso2  5728  poxp  6129  tfrlem5  6211  nndi  6382  nnmass  6383  findcard  6782  ac6sfi  6792  mulcanpig  7143  divgt0  8630  divge0  8631  uzind  9162  uzind2  9163  facavg  10492  prodfap0  11314  prodfrecap  11315  dvdsnprmd  11806  prmndvdsfaclt  11834  fiinopn  12171  neipsm  12323  tpnei  12329  opnneiid  12333  neibl  12660  tgqioo  12716