Theorem 3expib 1208

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

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

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 982

This theorem is referenced by:  3anidm12  1306  mob  2946  eqbrrdva  4837  funimaexglem  5342  fco  5426  f1oiso2  5877  caovimo  6121  smoel2  6370  nnaword  6578  3ecoptocl  6692  sbthlemi10  7041  distrnq0  7545  addassnq0  7548  prcdnql  7570  prcunqu  7571  genpdisj  7609  cauappcvgprlemrnd  7736  caucvgprlemrnd  7759  caucvgprprlemrnd  7787  nn0n0n1ge2b  9424  fzind  9460  icoshft  10084  fzen  10137  seq3coll  10953  shftuz  11001  mulgcd  12210  algcvga  12246  lcmneg  12269  isnmgm  13064  gsummgmpropd  13098  issgrpd  13116  iscmnd  13506  unitmulclb  13748  rmodislmodlem  13984  rmodislmod  13985  blssps  14771  blss  14772  metcnp3  14855  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173