Theorem 3expib 1185

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 1181	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 252	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103   ∧ 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:  3anidm12  1274  mob  2870  eqbrrdva  4717  funimaexglem  5214  fco  5296  f1oiso2  5736  caovimo  5972  smoel2  6208  nnaword  6415  3ecoptocl  6526  sbthlemi10  6862  distrnq0  7291  addassnq0  7294  prcdnql  7316  prcunqu  7317  genpdisj  7355  cauappcvgprlemrnd  7482  caucvgprlemrnd  7505  caucvgprprlemrnd  7533  nn0n0n1ge2b  9154  fzind  9190  icoshft  9803  fzen  9854  seq3coll  10617  shftuz  10621  mulgcd  11740  algcvga  11768  lcmneg  11791  blssps  12635  blss  12636  metcnp3  12719  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958