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  2998  eqbrrdva  4924  funimaexglem  5438  fco  5526  f1oiso2  5999  caovimo  6247  smoel2  6533  nnaword  6743  3ecoptocl  6857  rex2dom  7062  sbthlemi10  7235  distrnq0  7770  addassnq0  7773  prcdnql  7795  prcunqu  7796  genpdisj  7834  cauappcvgprlemrnd  7961  caucvgprlemrnd  7984  caucvgprprlemrnd  8012  nn0n0n1ge2b  9653  fzind  9689  icoshft  10319  fzen  10373  seq3coll  11207  shftuz  11495  mulgcd  12705  algcvga  12741  lcmneg  12764  isnmgm  13562  gsummgmpropd  13596  issgrpd  13614  iscmnd  14004  unitmulclb  14248  rmodislmodlem  14485  rmodislmod  14486  blssps  15279  blss  15280  metcnp3  15363  sincosq1sgn  15678  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  iswlkg  16311