Theorem 3expib 1209

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

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

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 983

This theorem is referenced by:  3anidm12  1308  mob  2956  eqbrrdva  4852  funimaexglem  5362  fco  5447  f1oiso2  5903  caovimo  6147  smoel2  6396  nnaword  6604  3ecoptocl  6718  rex2dom  6917  sbthlemi10  7075  distrnq0  7579  addassnq0  7582  prcdnql  7604  prcunqu  7605  genpdisj  7643  cauappcvgprlemrnd  7770  caucvgprlemrnd  7793  caucvgprprlemrnd  7821  nn0n0n1ge2b  9459  fzind  9495  icoshft  10119  fzen  10172  seq3coll  10994  shftuz  11172  mulgcd  12381  algcvga  12417  lcmneg  12440  isnmgm  13236  gsummgmpropd  13270  issgrpd  13288  iscmnd  13678  unitmulclb  13920  rmodislmodlem  14156  rmodislmod  14157  blssps  14943  blss  14944  metcnp3  15027  sincosq1sgn  15342  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345