Theorem syl112anc 1275

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

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
syl112anc.5	|- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl112anc	|- ( ph -> et )

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. 2 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 306	. 2 |- ( ph -> ( th /\ ta ) )
6		syl112anc.5	. 2 |- ( ( ps /\ ch /\ ( th /\ ta ) ) -> et )
7	1, 2, 5, 6	syl3anc 1271	1 |- ( ph -> et )

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:  fvun1  5708  caseinl  7281  caseinr  7282  reapmul1  8765  recrecap  8879  rec11rap  8881  divdivdivap  8883  dmdcanap  8892  ddcanap  8896  rerecclap  8900  div2negap  8905  divap1d  8971  divmulapd  8982  apdivmuld  8983  divmulap2d  8994  divmulap3d  8995  divassapd  8996  div12apd  8997  div23apd  8998  divdirapd  8999  divsubdirapd  9000  div11apd  9001  ltmul12a  9030  ltdiv1  9038  ltrec  9053  lt2msq1  9055  lediv2  9061  lediv23  9063  recp1lt1  9069  qapne  9863  xadd4d  10110  xleaddadd  10112  modqge0  10584  modqlt  10585  modqid  10601  expgt1  10829  nnlesq  10895  expnbnd  10915  facubnd  10997  pfxsuffeqwrdeq  11269  resqrexlemover  11561  mulcn2  11863  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  eftlub  12241  eflegeo  12252  sin01bnd  12308  cos01bnd  12309  eirraplem  12328  bitsmod  12507  bezoutlemnewy  12557  bezoutlemstep  12558  mulgcd  12577  mulgcddvds  12656  prmind2  12682  oddpwdclemxy  12731  oddpwdclemodd  12734  qnumgt0  12760  pcpremul  12856  fldivp1  12911  pcfaclem  12912  qexpz  12915  prmpwdvds  12918  pockthg  12920  4sqlem10  12950  4sqlem12  12965  4sqlem16  12969  4sqlem17  12970  ablsub4  13890  znrrg  14664  txdis  14991  txdis1cn  14992  xblm  15131  reeff1oleme  15486  tangtx  15552  cosordlem  15563  logdivlti  15595  apcxp2  15653  mersenne  15711  lgsdilem  15746  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem3  15836  2sqlem8  15842  apdifflemr  16587