Theorem syl22anc 1251

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 306	. 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 1248	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  f1oprg  5566  tfrexlem  6420  th3qlem1  6724  en2prd  6909  enpr2d  6911  ssenen  6948  phplem4dom  6959  phplem4on  6964  fiunsnnn  6978  findcard2sd  6989  unsnfi  7016  sbthlemi9  7067  endjusym  7198  endjudisj  7322  djuen  7323  ltanqg  7513  ltmnqg  7514  ltnnnq  7536  addcmpblnq0  7556  addlocprlemeqgt  7645  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  addcanprleml  7727  recexprlem1ssl  7746  caucvgprlemloc  7788  caucvgprprlemloccalc  7797  mulcmpblnr  7854  ltasrg  7883  recexgt0sr  7886  mulextsr1lem  7893  mulextsr1  7894  srpospr  7896  prsrlt  7900  ltpsrprg  7916  mappsrprg  7917  pitonnlem1p1  7959  recidpirq  7971  axpre-ltadd  7999  mulgt0d  8195  mul4d  8227  add4d  8241  add42d  8242  subcan  8327  addsub4d  8430  subadd4d  8431  sub4d  8432  2addsubd  8433  addsubeq4d  8434  muladdd  8488  mulsubd  8489  addgegt0d  8592  addgtge0d  8593  addge0d  8595  le2addd  8636  le2subd  8637  ltleaddd  8638  leltaddd  8639  lt2subd  8641  apreap  8660  apsym  8679  apcotr  8680  apadd1  8681  apneg  8684  mulext1  8685  mulap0r  8688  mulge0d  8694  mulap0d  8731  divdivdivap  8786  divcanap5  8787  divap0d  8879  recdivapd  8880  recdivap2d  8881  divcanap6d  8882  ddcanapd  8883  rec11apd  8884  divmuldivapd  8905  divmuleqapd  8906  subrecapd  8914  prodgt0  8925  lt2msq  8959  ledivdiv  8963  lediv12a  8967  recreclt  8973  divgt0d  9008  mulgt1d  9009  lemulge11d  9010  lemulge12d  9011  ltmul12ad  9014  lemul12ad  9015  lemul12bd  9016  nndivtr  9078  qreccl  9763  ledivdivd  9844  lediv12ad  9878  lt2mul2divd  9887  xlt2add  10002  xleaddadd  10009  iccss2  10066  iccssico2  10069  lincmb01cmp  10125  iccf1o  10126  fzrev2i  10208  qtri3or  10383  elicore  10409  2tnp1ge0ge0  10444  modqid  10494  q0mod  10500  q1mod  10501  modqabs  10502  modqadd1  10506  mulqaddmodid  10509  mulp1mod1  10510  modqmuladd  10511  modqmuladdnn0  10513  qnegmod  10514  m1modnnsub1  10515  addmodid  10517  modqm1p1mod0  10520  modqltm1p1mod  10521  modqmul1  10522  q2submod  10530  modifeq2int  10531  modaddmodup  10532  modaddmodlo  10533  modqaddmulmod  10536  modqsubdir  10538  modqeqmodmin  10539  modsumfzodifsn  10541  addmodlteq  10543  frecfzennn  10571  ser3mono  10632  expcl2lemap  10696  mulexpzap  10724  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  ltexp2a  10736  leexp2a  10737  sqdivap  10748  qsqeqor  10795  expnbnd  10808  expsubapd  10829  lt2sqd  10849  le2sqd  10850  sq11d  10851  apexp1  10863  bcp1nk  10907  hashunlem  10949  zfz1isolem1  10985  cjap  11217  cnreim  11289  resqrexlem1arp  11316  resqrexlemp1rp  11317  resqrexlemglsq  11333  abs00ap  11373  absext  11374  absexpzap  11391  absrele  11394  sqrtmuld  11480  sqrtsq2d  11481  sqrtled  11482  sqrtltd  11483  sqr11d  11484  abs3lemd  11512  minmax  11541  xrmaxiflemlub  11559  xrltmaxsup  11568  xrminmax  11576  xrbdtri  11587  climuni  11604  2clim  11612  addcn2  11621  mulcn2  11623  fsum3  11698  mptfzshft  11753  fsumrev  11754  fisum0diag2  11758  modfsummodlemstep  11768  binomlem  11794  mertenslemi1  11846  fprodrev  11930  efcllemp  11969  p1modz1  12105  dvds1  12164  dvdsext  12166  mulmoddvds  12174  oexpneg  12188  evennn02n  12193  evennn2n  12194  bitsinv1  12273  bezoutlemmo  12327  mulgcd  12337  dvdssqlem  12351  rpmulgcd2  12417  isprm6  12469  sqrt2irraplemnn  12501  sqrt2irrap  12502  crth  12546  eulerthlemh  12553  prmdiveq  12558  powm2modprm  12575  modprm0  12577  pythagtriplem2  12589  pythagtriplem11  12597  pythagtriplem13  12599  pythagtrip  12606  pcid  12647  pcgcd1  12651  pcprmpw2  12656  dvdsprmpweqle  12660  pcaddlem  12662  pcadd  12663  fldivp1  12671  4sqlem12  12725  4sqlem14  12727  4sqlem15  12728  4sqlem16  12729  unennn  12768  ennnfonelemg  12774  ennnfonelemhf1o  12784  inffinp1  12800  isstructr  12847  setscomd  12873  imasbas  13139  imasplusg  13140  imasmulr  13141  subm0  13314  lssvancl1  14129  lssvnegcl  14138  lspprvacl  14175  lspsneli  14177  lspsn  14178  znf1o  14413  ntrin  14596  topssnei  14634  restbasg  14640  cnntri  14696  txcn  14747  txlm  14751  cnmpt2res  14769  psmetlecl  14806  xmetlecl  14839  bldisj  14873  bdmet  14974  bdbl  14975  bdmopn  14976  xmetxp  14979  metcnp  14984  tgioo  15026  cncfmet  15064  dedekindeulemlub  15092  suplociccreex  15096  ellimc3apf  15132  limcimolemlt  15136  limccnp2cntop  15149  dvfvalap  15153  dvidsslem  15165  dvmulxxbr  15174  dvaddxx  15175  dvmulxx  15176  dviaddf  15177  dvimulf  15178  dvcoapbr  15179  dvmptclx  15190  cxplt3  15392  cxpltd  15400  cxpled  15401  cxplt3d  15407  cxple3d  15408  logbrec  15432  logbgcd1irraplemap  15441  wilthlem1  15452  mpodvdsmulf1o  15462  lgslem1  15477  lgslem3  15479  lgsdirprm  15511  gausslemma2dlem1f1o  15537  gausslemma2dlem6  15544  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem4  15550  lgseisen  15551  lgsquadlem1  15554  lgsquad2lem1  15558  lgsquad3  15561  m1lgs  15562  2lgslem1a1  15563  2sqlem7  15598