Theorem 3expib 1237

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

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

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 1011

This theorem is referenced by:  3anidm12  1336  mob  3008  eqbrrdva  4948  funimaexglem  5462  fco  5550  f1oiso2  6027  caovimo  6277  smoel2  6568  nnaword  6778  3ecoptocl  6892  rex2dom  7104  sbthlemi10  7277  distrnq0  7820  addassnq0  7823  prcdnql  7845  prcunqu  7846  genpdisj  7884  cauappcvgprlemrnd  8011  caucvgprlemrnd  8034  caucvgprprlemrnd  8062  nn0n0n1ge2b  9708  fzind  9744  icoshft  10375  fzen  10430  seq3coll  11277  shftuz  11565  mulgcd  12776  algcvga  12812  lcmneg  12835  isnmgm  13663  issgrpd  13710  iscmnd  14084  unitmulclb  14404  rmodislmodlem  14670  rmodislmod  14671  blssps  15511  blss  15512  metcnp3  15595  sincosq1sgn  15910  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  iswlkg  16553  lealltlt1  16734