Theorem syl112anc 1185

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 301	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1181	1 ⊢ (𝜑 → 𝜂)

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

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 929

This theorem is referenced by:  fvun1  5405  caseinl  6862  reapmul1  8169  recrecap  8273  rec11rap  8275  divdivdivap  8277  dmdcanap  8286  ddcanap  8290  rerecclap  8294  div2negap  8299  divap1d  8365  divmulapd  8376  apdivmuld  8377  divmulap2d  8388  divmulap3d  8389  divassapd  8390  div12apd  8391  div23apd  8392  divdirapd  8393  divsubdirapd  8394  div11apd  8395  ltmul12a  8418  ltdiv1  8426  ltrec  8441  lt2msq1  8443  lediv2  8449  lediv23  8451  recp1lt1  8457  qapne  9223  xadd4d  9451  xleaddadd  9453  modqge0  9888  modqlt  9889  modqid  9905  expgt1  10124  nnlesq  10189  expnbnd  10208  facubnd  10284  resqrexlemover  10574  mulcn2  10871  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  eftlub  11145  eflegeo  11157  sin01bnd  11213  cos01bnd  11214  eirraplem  11229  bezoutlemnewy  11428  bezoutlemstep  11429  mulgcd  11448  mulgcddvds  11519  prmind2  11545  oddpwdclemxy  11590  oddpwdclemodd  11593  qnumgt0  11619  xblm  12219