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  2986  eqbrrdva  4898  funimaexglem  5410  fco  5497  f1oiso2  5963  caovimo  6211  smoel2  6464  nnaword  6674  3ecoptocl  6788  rex2dom  6991  sbthlemi10  7159  distrnq0  7672  addassnq0  7675  prcdnql  7697  prcunqu  7698  genpdisj  7736  cauappcvgprlemrnd  7863  caucvgprlemrnd  7886  caucvgprprlemrnd  7914  nn0n0n1ge2b  9552  fzind  9588  icoshft  10218  fzen  10271  seq3coll  11099  shftuz  11371  mulgcd  12580  algcvga  12616  lcmneg  12639  isnmgm  13436  gsummgmpropd  13470  issgrpd  13488  iscmnd  13878  unitmulclb  14121  rmodislmodlem  14357  rmodislmod  14358  blssps  15144  blss  15145  metcnp3  15228  sincosq1sgn  15543  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  iswlkg  16140