Theorem 3expib 1188

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 1184	. 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  1277  mob  2894  eqbrrdva  4756  funimaexglem  5253  fco  5335  f1oiso2  5777  caovimo  6014  smoel2  6250  nnaword  6458  3ecoptocl  6569  sbthlemi10  6910  distrnq0  7379  addassnq0  7382  prcdnql  7404  prcunqu  7405  genpdisj  7443  cauappcvgprlemrnd  7570  caucvgprlemrnd  7593  caucvgprprlemrnd  7621  nn0n0n1ge2b  9243  fzind  9279  icoshft  9894  fzen  9945  seq3coll  10713  shftuz  10717  mulgcd  11900  algcvga  11928  lcmneg  11951  blssps  12838  blss  12839  metcnp3  12922  sincosq1sgn  13158  sincosq2sgn  13159  sincosq3sgn  13160  sincosq4sgn  13161