Theorem 3expib 1206

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

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

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 980

This theorem is referenced by:  3anidm12  1295  mob  2921  eqbrrdva  4799  funimaexglem  5301  fco  5383  f1oiso2  5830  caovimo  6070  smoel2  6306  nnaword  6514  3ecoptocl  6626  sbthlemi10  6967  distrnq0  7460  addassnq0  7463  prcdnql  7485  prcunqu  7486  genpdisj  7524  cauappcvgprlemrnd  7651  caucvgprlemrnd  7674  caucvgprprlemrnd  7702  nn0n0n1ge2b  9334  fzind  9370  icoshft  9992  fzen  10045  seq3coll  10824  shftuz  10828  mulgcd  12019  algcvga  12053  lcmneg  12076  isnmgm  12784  iscmnd  13106  unitmulclb  13288  rmodislmodlem  13445  rmodislmod  13446  blssps  14012  blss  14013  metcnp3  14096  sincosq1sgn  14332  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335