Theorem 3expib 1233

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

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

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 1007

This theorem is referenced by:  3anidm12  1332  mob  3001  eqbrrdva  4927  funimaexglem  5441  fco  5529  f1oiso2  6002  caovimo  6250  smoel2  6536  nnaword  6746  3ecoptocl  6860  rex2dom  7065  sbthlemi10  7238  distrnq0  7779  addassnq0  7782  prcdnql  7804  prcunqu  7805  genpdisj  7843  cauappcvgprlemrnd  7970  caucvgprlemrnd  7993  caucvgprprlemrnd  8021  nn0n0n1ge2b  9663  fzind  9699  icoshft  10329  fzen  10383  seq3coll  11222  shftuz  11510  mulgcd  12720  algcvga  12756  lcmneg  12779  isnmgm  13594  gsummgmpropd  13628  issgrpd  13646  iscmnd  14036  unitmulclb  14281  rmodislmodlem  14547  rmodislmod  14548  blssps  15341  blss  15342  metcnp3  15425  sincosq1sgn  15740  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  iswlkg  16373