Theorem 3expib 1147

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 925

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  3anidm12  1232  mob  2798  eqbrrdva  4619  funimaexglem  5110  fco  5189  f1oiso2  5620  caovimo  5852  smoel2  6082  nnaword  6284  3ecoptocl  6395  sbthlemi10  6729  distrnq0  7072  addassnq0  7075  prcdnql  7097  prcunqu  7098  genpdisj  7136  cauappcvgprlemrnd  7263  caucvgprlemrnd  7286  caucvgprprlemrnd  7314  nn0n0n1ge2b  8880  fzind  8915  icoshft  9461  fzen  9511  iseqcoll  10301  shftuz  10305  mulgcd  11337  algcvga  11365  lcmneg  11388