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  4836  funimaexglem  5341  fco  5423  f1oiso2  5874  caovimo  6117  smoel2  6361  nnaword  6569  3ecoptocl  6683  sbthlemi10  7032  distrnq0  7526  addassnq0  7529  prcdnql  7551  prcunqu  7552  genpdisj  7590  cauappcvgprlemrnd  7717  caucvgprlemrnd  7740  caucvgprprlemrnd  7768  nn0n0n1ge2b  9405  fzind  9441  icoshft  10065  fzen  10118  seq3coll  10934  shftuz  10982  mulgcd  12183  algcvga  12219  lcmneg  12242  isnmgm  13003  gsummgmpropd  13037  issgrpd  13055  iscmnd  13428  unitmulclb  13670  rmodislmodlem  13906  rmodislmod  13907  blssps  14663  blss  14664  metcnp3  14747  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065