Theorem syl112anc 1232

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  fvun1  5552  caseinl  7056  caseinr  7057  reapmul1  8493  recrecap  8605  rec11rap  8607  divdivdivap  8609  dmdcanap  8618  ddcanap  8622  rerecclap  8626  div2negap  8631  divap1d  8697  divmulapd  8708  apdivmuld  8709  divmulap2d  8720  divmulap3d  8721  divassapd  8722  div12apd  8723  div23apd  8724  divdirapd  8725  divsubdirapd  8726  div11apd  8727  ltmul12a  8755  ltdiv1  8763  ltrec  8778  lt2msq1  8780  lediv2  8786  lediv23  8788  recp1lt1  8794  qapne  9577  xadd4d  9821  xleaddadd  9823  modqge0  10267  modqlt  10268  modqid  10284  expgt1  10493  nnlesq  10558  expnbnd  10578  facubnd  10658  resqrexlemover  10952  mulcn2  11253  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  eftlub  11631  eflegeo  11642  sin01bnd  11698  cos01bnd  11699  eirraplem  11717  bezoutlemnewy  11929  bezoutlemstep  11930  mulgcd  11949  mulgcddvds  12026  prmind2  12052  oddpwdclemxy  12101  oddpwdclemodd  12104  qnumgt0  12130  pcpremul  12225  fldivp1  12278  pcfaclem  12279  qexpz  12282  prmpwdvds  12285  pockthg  12287  4sqlem10  12317  txdis  12927  txdis1cn  12928  xblm  13067  reeff1oleme  13343  tangtx  13409  cosordlem  13420  logdivlti  13452  apcxp2  13508  lgsdilem  13578  2sqlem3  13603  2sqlem8  13609  apdifflemr  13936