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  3002  eqbrrdva  4930  funimaexglem  5444  fco  5532  f1oiso2  6006  caovimo  6256  smoel2  6547  nnaword  6757  3ecoptocl  6871  rex2dom  7076  sbthlemi10  7249  distrnq0  7790  addassnq0  7793  prcdnql  7815  prcunqu  7816  genpdisj  7854  cauappcvgprlemrnd  7981  caucvgprlemrnd  8004  caucvgprprlemrnd  8032  nn0n0n1ge2b  9678  fzind  9714  icoshft  10345  fzen  10400  seq3coll  11242  shftuz  11530  mulgcd  12740  algcvga  12776  lcmneg  12799  isnmgm  13626  gsummgmpropd  13660  issgrpd  13678  iscmnd  14054  unitmulclb  14362  rmodislmodlem  14627  rmodislmod  14628  blssps  15421  blss  15422  metcnp3  15505  sincosq1sgn  15820  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  iswlkg  16453  lealltlt1  16634