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  2985  eqbrrdva  4892  funimaexglem  5404  fco  5491  f1oiso2  5957  caovimo  6205  smoel2  6455  nnaword  6665  3ecoptocl  6779  rex2dom  6979  sbthlemi10  7141  distrnq0  7654  addassnq0  7657  prcdnql  7679  prcunqu  7680  genpdisj  7718  cauappcvgprlemrnd  7845  caucvgprlemrnd  7868  caucvgprprlemrnd  7896  nn0n0n1ge2b  9534  fzind  9570  icoshft  10194  fzen  10247  seq3coll  11072  shftuz  11336  mulgcd  12545  algcvga  12581  lcmneg  12604  isnmgm  13401  gsummgmpropd  13435  issgrpd  13453  iscmnd  13843  unitmulclb  14086  rmodislmodlem  14322  rmodislmod  14323  blssps  15109  blss  15110  metcnp3  15193  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  iswlkg  16050