Theorem syl112anc 1139

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl112anc.5	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl112anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. 2 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 290	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1135	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  fvun1  5239  reapmul1  7584  recrecap  7683  rec11rap  7685  divdivdivap  7687  dmdcanap  7696  ddcanap  7700  rerecclap  7704  div2negap  7709  divap1d  7774  divmulapd  7785  divmulap2d  7796  divmulap3d  7797  divassapd  7798  div12apd  7799  div23apd  7800  divdirapd  7801  divsubdirapd  7802  div11apd  7803  ltmul12a  7824  ltdiv1  7832  ltrec  7847  lt2msq1  7849  lediv2  7855  lediv23  7857  recp1lt1  7863  qapne  8572  modqge0  9172  modqlt  9173  expgt1  9291  nnlesq  9354  expnbnd  9370  resqrexlemover  9606  mulcn2  9831