Theorem 3expib 1207

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

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

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 981

This theorem is referenced by:  3anidm12  1305  mob  2931  eqbrrdva  4809  funimaexglem  5311  fco  5393  f1oiso2  5841  caovimo  6082  smoel2  6318  nnaword  6526  3ecoptocl  6638  sbthlemi10  6979  distrnq0  7472  addassnq0  7475  prcdnql  7497  prcunqu  7498  genpdisj  7536  cauappcvgprlemrnd  7663  caucvgprlemrnd  7686  caucvgprprlemrnd  7714  nn0n0n1ge2b  9346  fzind  9382  icoshft  10004  fzen  10057  seq3coll  10836  shftuz  10840  mulgcd  12031  algcvga  12065  lcmneg  12088  isnmgm  12798  issgrpd  12837  iscmnd  13192  unitmulclb  13419  rmodislmodlem  13596  rmodislmod  13597  blssps  14280  blss  14281  metcnp3  14364  sincosq1sgn  14600  sincosq2sgn  14601  sincosq3sgn  14602  sincosq4sgn  14603