Theorem 3expib 1230

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

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

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 1004

This theorem is referenced by:  3anidm12  1329  mob  2985  eqbrrdva  4895  funimaexglem  5407  fco  5494  f1oiso2  5960  caovimo  6208  smoel2  6460  nnaword  6670  3ecoptocl  6784  rex2dom  6984  sbthlemi10  7149  distrnq0  7662  addassnq0  7665  prcdnql  7687  prcunqu  7688  genpdisj  7726  cauappcvgprlemrnd  7853  caucvgprlemrnd  7876  caucvgprprlemrnd  7904  nn0n0n1ge2b  9542  fzind  9578  icoshft  10203  fzen  10256  seq3coll  11082  shftuz  11349  mulgcd  12558  algcvga  12594  lcmneg  12617  isnmgm  13414  gsummgmpropd  13448  issgrpd  13466  iscmnd  13856  unitmulclb  14099  rmodislmodlem  14335  rmodislmod  14336  blssps  15122  blss  15123  metcnp3  15206  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  iswlkg  16101