Theorem 3expib 1211

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

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

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 985

This theorem is referenced by:  3anidm12  1310  mob  2965  eqbrrdva  4869  funimaexglem  5380  fco  5465  f1oiso2  5924  caovimo  6170  smoel2  6419  nnaword  6627  3ecoptocl  6741  rex2dom  6941  sbthlemi10  7101  distrnq0  7614  addassnq0  7617  prcdnql  7639  prcunqu  7640  genpdisj  7678  cauappcvgprlemrnd  7805  caucvgprlemrnd  7828  caucvgprprlemrnd  7856  nn0n0n1ge2b  9494  fzind  9530  icoshft  10154  fzen  10207  seq3coll  11031  shftuz  11294  mulgcd  12503  algcvga  12539  lcmneg  12562  isnmgm  13359  gsummgmpropd  13393  issgrpd  13411  iscmnd  13801  unitmulclb  14043  rmodislmodlem  14279  rmodislmod  14280  blssps  15066  blss  15067  metcnp3  15150  sincosq1sgn  15465  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468