Theorem 3expib 1237

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anidm12  1336  mob  3008  eqbrrdva  4950  funimaexglem  5464  fco  5552  f1oiso2  6033  caovimo  6283  smoel2  6574  nnaword  6784  3ecoptocl  6898  rex2dom  7110  sbthlemi10  7283  distrnq0  7826  addassnq0  7829  prcdnql  7851  prcunqu  7852  genpdisj  7890  cauappcvgprlemrnd  8017  caucvgprlemrnd  8040  caucvgprprlemrnd  8068  nn0n0n1ge2b  9727  fzind  9763  icoshft  10394  fzen  10449  seq3coll  11296  shftuz  11584  mulgcd  12795  algcvga  12831  lcmneg  12854  isnmgm  13682  issgrpd  13729  iscmnd  14103  unitmulclb  14423  rmodislmodlem  14689  rmodislmod  14690  blssps  15530  blss  15531  metcnp3  15614  sincosq1sgn  15930  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  bcmono  16124  iswlkg  16582  lealltlt1  16763