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  2987  eqbrrdva  4902  funimaexglem  5415  fco  5502  f1oiso2  5973  caovimo  6221  smoel2  6474  nnaword  6684  3ecoptocl  6798  rex2dom  7001  sbthlemi10  7170  distrnq0  7684  addassnq0  7687  prcdnql  7709  prcunqu  7710  genpdisj  7748  cauappcvgprlemrnd  7875  caucvgprlemrnd  7898  caucvgprprlemrnd  7926  nn0n0n1ge2b  9564  fzind  9600  icoshft  10230  fzen  10283  seq3coll  11112  shftuz  11400  mulgcd  12610  algcvga  12646  lcmneg  12669  isnmgm  13466  gsummgmpropd  13500  issgrpd  13518  iscmnd  13908  unitmulclb  14152  rmodislmodlem  14388  rmodislmod  14389  blssps  15180  blss  15181  metcnp3  15264  sincosq1sgn  15579  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  iswlkg  16209