Theorem syl22anc 1229

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 1226	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  5475  tfrexlem  6298  th3qlem1  6599  enpr2d  6779  ssenen  6813  phplem4dom  6824  phplem4on  6829  fiunsnnn  6843  findcard2sd  6854  unsnfi  6880  sbthlemi9  6926  endjusym  7057  endjudisj  7162  djuen  7163  ltanqg  7337  ltmnqg  7338  ltnnnq  7360  addcmpblnq0  7380  addlocprlemeqgt  7469  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  addcanprleml  7551  recexprlem1ssl  7570  caucvgprlemloc  7612  caucvgprprlemloccalc  7621  mulcmpblnr  7678  ltasrg  7707  recexgt0sr  7710  mulextsr1lem  7717  mulextsr1  7718  srpospr  7720  prsrlt  7724  ltpsrprg  7740  mappsrprg  7741  pitonnlem1p1  7783  recidpirq  7795  axpre-ltadd  7823  mulgt0d  8017  mul4d  8049  add4d  8063  add42d  8064  subcan  8149  addsub4d  8252  subadd4d  8253  sub4d  8254  2addsubd  8255  addsubeq4d  8256  muladdd  8310  mulsubd  8311  addgegt0d  8413  addgtge0d  8414  addge0d  8416  le2addd  8457  le2subd  8458  ltleaddd  8459  leltaddd  8460  lt2subd  8462  apreap  8481  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  mulap0r  8509  mulge0d  8515  mulap0d  8551  divdivdivap  8605  divcanap5  8606  divap0d  8698  recdivapd  8699  recdivap2d  8700  divcanap6d  8701  ddcanapd  8702  rec11apd  8703  divmuldivapd  8724  divmuleqapd  8725  subrecapd  8733  prodgt0  8743  lt2msq  8777  ledivdiv  8781  lediv12a  8785  recreclt  8791  divgt0d  8826  mulgt1d  8827  lemulge11d  8828  lemulge12d  8829  ltmul12ad  8832  lemul12ad  8833  lemul12bd  8834  nndivtr  8895  qreccl  9576  ledivdivd  9654  lediv12ad  9688  lt2mul2divd  9697  xlt2add  9812  xleaddadd  9819  iccss2  9876  iccssico2  9879  lincmb01cmp  9935  iccf1o  9936  fzrev2i  10017  qtri3or  10174  elicore  10198  2tnp1ge0ge0  10232  modqid  10280  q0mod  10286  q1mod  10287  modqabs  10288  modqadd1  10292  mulqaddmodid  10295  mulp1mod1  10296  modqmuladd  10297  modqmuladdnn0  10299  qnegmod  10300  m1modnnsub1  10301  addmodid  10303  modqm1p1mod0  10306  modqltm1p1mod  10307  modqmul1  10308  q2submod  10316  modifeq2int  10317  modaddmodup  10318  modaddmodlo  10319  modqaddmulmod  10322  modqsubdir  10324  modqeqmodmin  10325  modsumfzodifsn  10327  addmodlteq  10329  frecfzennn  10357  ser3mono  10409  expcl2lemap  10463  mulexpzap  10491  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  ltexp2a  10503  leexp2a  10504  sqdivap  10515  qsqeqor  10561  expnbnd  10574  expsubapd  10595  lt2sqd  10615  le2sqd  10616  sq11d  10617  apexp1  10627  bcp1nk  10671  hashunlem  10713  zfz1isolem1  10749  cjap  10844  cnreim  10916  resqrexlem1arp  10943  resqrexlemp1rp  10944  resqrexlemglsq  10960  abs00ap  11000  absext  11001  absexpzap  11018  absrele  11021  sqrtmuld  11107  sqrtsq2d  11108  sqrtled  11109  sqrtltd  11110  sqr11d  11111  abs3lemd  11139  minmax  11167  xrmaxiflemlub  11185  xrltmaxsup  11194  xrminmax  11202  xrbdtri  11213  climuni  11230  2clim  11238  addcn2  11247  mulcn2  11249  fsum3  11324  mptfzshft  11379  fsumrev  11380  fisum0diag2  11384  modfsummodlemstep  11394  binomlem  11420  mertenslemi1  11472  fprodrev  11556  efcllemp  11595  p1modz1  11730  dvds1  11787  dvdsext  11789  mulmoddvds  11797  oexpneg  11810  evennn02n  11815  evennn2n  11816  bezoutlemmo  11935  mulgcd  11945  dvdssqlem  11959  rpmulgcd2  12023  isprm6  12075  sqrt2irraplemnn  12107  sqrt2irrap  12108  crth  12152  eulerthlemh  12159  prmdiveq  12164  powm2modprm  12180  modprm0  12182  pythagtriplem2  12194  pythagtriplem11  12202  pythagtriplem13  12204  pythagtrip  12211  pcid  12251  pcgcd1  12255  pcprmpw2  12260  dvdsprmpweqle  12264  pcaddlem  12266  pcadd  12267  fldivp1  12274  unennn  12326  ennnfonelemg  12332  ennnfonelemhf1o  12342  inffinp1  12358  isstructr  12405  ntrin  12724  topssnei  12762  restbasg  12768  cnntri  12824  txcn  12875  txlm  12879  cnmpt2res  12897  psmetlecl  12934  xmetlecl  12967  bldisj  13001  bdmet  13102  bdbl  13103  bdmopn  13104  xmetxp  13107  metcnp  13112  tgioo  13146  cncfmet  13179  dedekindeulemlub  13198  suplociccreex  13202  ellimc3apf  13229  limcimolemlt  13233  limccnp2cntop  13246  dvfvalap  13250  dvmulxxbr  13266  dvaddxx  13267  dvmulxx  13268  dviaddf  13269  dvimulf  13270  dvcoapbr  13271  dvmptclx  13280  cxplt3  13440  cxpltd  13448  cxpled  13449  cxplt3d  13454  cxple3d  13455  logbrec  13478  logbgcd1irraplemap  13487  lgslem1  13501  lgslem3  13503  lgsdirprm  13535  2sqlem7  13557