Theorem 3expib 1232

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1228	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 254	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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 1006

This theorem is referenced by:  3anidm12  1331  mob  2988  eqbrrdva  4900  funimaexglem  5413  fco  5500  f1oiso2  5968  caovimo  6216  smoel2  6469  nnaword  6679  3ecoptocl  6793  rex2dom  6996  sbthlemi10  7165  distrnq0  7679  addassnq0  7682  prcdnql  7704  prcunqu  7705  genpdisj  7743  cauappcvgprlemrnd  7870  caucvgprlemrnd  7893  caucvgprprlemrnd  7921  nn0n0n1ge2b  9559  fzind  9595  icoshft  10225  fzen  10278  seq3coll  11107  shftuz  11379  mulgcd  12589  algcvga  12625  lcmneg  12648  isnmgm  13445  gsummgmpropd  13479  issgrpd  13497  iscmnd  13887  unitmulclb  14131  rmodislmodlem  14367  rmodislmod  14368  blssps  15154  blss  15155  metcnp3  15238  sincosq1sgn  15553  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  iswlkg  16183