Theorem syl22anc 1218

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 )
syl22anc.5	|- ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl22anc	|- ( ph -> et )

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 304	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylXanc.3	. 2 |- ( ph -> th )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		syl22anc.5	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et )
7	3, 4, 5, 6	syl12anc 1215	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  f1oprg  5419  tfrexlem  6239  th3qlem1  6539  enpr2d  6719  ssenen  6753  phplem4dom  6764  phplem4on  6769  fiunsnnn  6783  findcard2sd  6794  unsnfi  6815  sbthlemi9  6861  endjusym  6989  endjudisj  7083  djuen  7084  ltanqg  7232  ltmnqg  7233  ltnnnq  7255  addcmpblnq0  7275  addlocprlemeqgt  7364  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  addcanprleml  7446  recexprlem1ssl  7465  caucvgprlemloc  7507  caucvgprprlemloccalc  7516  mulcmpblnr  7573  ltasrg  7602  recexgt0sr  7605  mulextsr1lem  7612  mulextsr1  7613  srpospr  7615  prsrlt  7619  ltpsrprg  7635  mappsrprg  7636  pitonnlem1p1  7678  recidpirq  7690  axpre-ltadd  7718  mulgt0d  7909  mul4d  7941  add4d  7955  add42d  7956  subcan  8041  addsub4d  8144  subadd4d  8145  sub4d  8146  2addsubd  8147  addsubeq4d  8148  muladdd  8202  mulsubd  8203  addgegt0d  8305  addgtge0d  8306  addge0d  8308  le2addd  8349  le2subd  8350  ltleaddd  8351  leltaddd  8352  lt2subd  8354  apreap  8373  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  mulap0r  8401  mulge0d  8407  mulap0d  8443  divdivdivap  8497  divcanap5  8498  divap0d  8590  recdivapd  8591  recdivap2d  8592  divcanap6d  8593  ddcanapd  8594  rec11apd  8595  divmuldivapd  8616  subrecapd  8624  prodgt0  8634  lt2msq  8668  ledivdiv  8672  lediv12a  8676  recreclt  8682  divgt0d  8717  mulgt1d  8718  lemulge11d  8719  lemulge12d  8720  ltmul12ad  8723  lemul12ad  8724  lemul12bd  8725  nndivtr  8786  qreccl  9461  ledivdivd  9539  lediv12ad  9573  lt2mul2divd  9582  xlt2add  9693  xleaddadd  9700  iccss2  9757  iccssico2  9760  lincmb01cmp  9816  iccf1o  9817  fzrev2i  9897  qtri3or  10051  2tnp1ge0ge0  10105  modqid  10153  q0mod  10159  q1mod  10160  modqabs  10161  modqadd1  10165  mulqaddmodid  10168  mulp1mod1  10169  modqmuladd  10170  modqmuladdnn0  10172  qnegmod  10173  m1modnnsub1  10174  addmodid  10176  modqm1p1mod0  10179  modqltm1p1mod  10180  modqmul1  10181  q2submod  10189  modifeq2int  10190  modaddmodup  10191  modaddmodlo  10192  modqaddmulmod  10195  modqsubdir  10197  modqeqmodmin  10198  modsumfzodifsn  10200  addmodlteq  10202  frecfzennn  10230  ser3mono  10282  expcl2lemap  10336  mulexpzap  10364  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  ltexp2a  10376  leexp2a  10377  sqdivap  10388  expnbnd  10446  expsubapd  10466  lt2sqd  10486  le2sqd  10487  sq11d  10488  apexp1  10496  bcp1nk  10540  hashunlem  10582  zfz1isolem1  10615  cjap  10710  cnreim  10782  resqrexlem1arp  10809  resqrexlemp1rp  10810  resqrexlemglsq  10826  abs00ap  10866  absext  10867  absexpzap  10884  absrele  10887  sqrtmuld  10973  sqrtsq2d  10974  sqrtled  10975  sqrtltd  10976  sqr11d  10977  abs3lemd  11005  minmax  11033  xrmaxiflemlub  11049  xrltmaxsup  11058  xrminmax  11066  xrbdtri  11077  climuni  11094  2clim  11102  addcn2  11111  mulcn2  11113  fsum3  11188  mptfzshft  11243  fsumrev  11244  fisum0diag2  11248  modfsummodlemstep  11258  binomlem  11284  mertenslemi1  11336  efcllemp  11401  dvds1  11587  dvdsext  11589  mulmoddvds  11597  oexpneg  11610  evennn02n  11615  evennn2n  11616  bezoutlemmo  11730  mulgcd  11740  dvdssqlem  11754  rpmulgcd2  11812  isprm6  11861  sqrt2irraplemnn  11893  sqrt2irrap  11894  crth  11936  unennn  11946  ennnfonelemg  11952  ennnfonelemhf1o  11962  inffinp1  11978  isstructr  12013  ntrin  12332  topssnei  12370  restbasg  12376  cnntri  12432  txcn  12483  txlm  12487  cnmpt2res  12505  psmetlecl  12542  xmetlecl  12575  bldisj  12609  bdmet  12710  bdbl  12711  bdmopn  12712  xmetxp  12715  metcnp  12720  tgioo  12754  cncfmet  12787  dedekindeulemlub  12806  suplociccreex  12810  ellimc3apf  12837  limcimolemlt  12841  limccnp2cntop  12854  dvfvalap  12858  dvmulxxbr  12874  dvaddxx  12875  dvmulxx  12876  dviaddf  12877  dvimulf  12878  dvcoapbr  12879  dvmptclx  12888  cxplt3  13048  cxpltd  13056  cxpled  13057  cxplt3d  13062  cxple3d  13063  logbrec  13085  logbgcd1irraplemap  13094