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  4952  funimaexglem  5467  fco  5555  f1oiso2  6036  caovimo  6286  smoel2  6578  nnaword  6788  3ecoptocl  6902  rex2dom  7115  sbthlemi10  7289  distrnq0  7833  addassnq0  7836  prcdnql  7858  prcunqu  7859  genpdisj  7897  cauappcvgprlemrnd  8024  caucvgprlemrnd  8047  caucvgprprlemrnd  8075  nn0n0n1ge2b  9737  fzind  9773  icoshft  10410  fzen  10465  seq3coll  11317  shftuz  11605  mulgcd  12819  algcvga  12855  lcmneg  12878  isnmgm  13740  issgrpd  13787  iscmnd  14192  unitmulclb  14531  rmodislmodlem  14797  rmodislmod  14798  blssps  15665  blss  15666  metcnp3  15749  sincosq1sgn  16065  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  bcmono  16316  iswlkg  16787  lealltlt1  16968