Theorem syl22anc 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 )
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 1272	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  5660  tfrexlem  6565  th3qlem1  6871  en2prd  7059  enpr2d  7064  ssenen  7105  phplem4dom  7116  phplem4on  7122  fiunsnnn  7138  findcard2sd  7149  unsnfi  7179  sbthlemi9  7235  fsuppcorn  7254  endjusym  7387  endjudisj  7517  djuen  7518  ltanqg  7715  ltmnqg  7716  ltnnnq  7738  addcmpblnq0  7758  addlocprlemeqgt  7847  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  addcanprleml  7929  recexprlem1ssl  7948  caucvgprlemloc  7990  caucvgprprlemloccalc  7999  mulcmpblnr  8056  ltasrg  8085  recexgt0sr  8088  mulextsr1lem  8095  mulextsr1  8096  srpospr  8098  prsrlt  8102  ltpsrprg  8118  mappsrprg  8119  pitonnlem1p1  8161  recidpirq  8173  axpre-ltadd  8201  mulgt0d  8396  mul4d  8428  add4d  8442  add42d  8443  subcan  8528  addsub4d  8631  subadd4d  8632  sub4d  8633  2addsubd  8634  addsubeq4d  8635  muladdd  8689  mulsubd  8690  addgegt0d  8793  addgtge0d  8794  addge0d  8796  le2addd  8837  le2subd  8838  ltleaddd  8839  leltaddd  8840  lt2subd  8842  apreap  8861  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  mulap0r  8889  mulge0d  8895  mulap0d  8932  divdivdivap  8987  divcanap5  8988  divap0d  9080  recdivapd  9081  recdivap2d  9082  divcanap6d  9083  ddcanapd  9084  rec11apd  9085  divmuldivapd  9106  divmuleqapd  9107  subrecapd  9115  prodgt0  9126  lt2msq  9160  ledivdiv  9164  lediv12a  9168  recreclt  9174  divgt0d  9209  mulgt1d  9210  lemulge11d  9211  lemulge12d  9212  ltmul12ad  9215  lemul12ad  9216  lemul12bd  9217  nndivtr  9279  qreccl  9974  ledivdivd  10055  lediv12ad  10089  lt2mul2divd  10098  xlt2add  10213  xleaddadd  10220  iccss2  10277  iccssico2  10280  lincmb01cmp  10336  iccf1o  10338  fzrev2i  10420  qtri3or  10600  elicore  10626  2tnp1ge0ge0  10661  modqid  10711  q0mod  10717  q1mod  10718  modqabs  10719  modqadd1  10723  mulqaddmodid  10726  mulp1mod1  10727  modqmuladd  10728  modqmuladdnn0  10730  qnegmod  10731  m1modnnsub1  10732  addmodid  10734  modqm1p1mod0  10737  modqltm1p1mod  10738  modqmul1  10739  q2submod  10747  modifeq2int  10748  modaddmodup  10749  modaddmodlo  10750  modqaddmulmod  10753  modqsubdir  10755  modqeqmodmin  10756  modsumfzodifsn  10758  addmodlteq  10760  frecfzennn  10788  ser3mono  10849  expcl2lemap  10913  mulexpzap  10941  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  ltexp2a  10953  leexp2a  10954  sqdivap  10965  qsqeqor  11012  expnbnd  11025  expsubapd  11046  lt2sqd  11066  le2sqd  11067  sq11d  11068  apexp1  11080  bcp1nk  11124  hashunlem  11168  zfz1isolem1  11212  hashtpgim  11217  cjap  11591  cnreim  11663  resqrexlem1arp  11690  resqrexlemp1rp  11691  resqrexlemglsq  11707  abs00ap  11747  absext  11748  absexpzap  11765  absrele  11768  sqrtmuld  11854  sqrtsq2d  11855  sqrtled  11856  sqrtltd  11857  sqr11d  11858  abs3lemd  11886  minmax  11915  xrmaxiflemlub  11933  xrltmaxsup  11942  xrminmax  11950  xrbdtri  11961  climuni  11978  2clim  11986  addcn2  11995  mulcn2  11997  fsum3  12073  mptfzshft  12128  fsumrev  12129  fisum0diag2  12133  modfsummodlemstep  12143  binomlem  12169  mertenslemi1  12221  fprodrev  12305  efcllemp  12344  p1modz1  12480  dvds1  12539  dvdsext  12541  mulmoddvds  12549  oexpneg  12563  evennn02n  12568  evennn2n  12569  bitsinv1  12648  bezoutlemmo  12702  mulgcd  12712  dvdssqlem  12726  rpmulgcd2  12792  isprm6  12844  sqrt2irraplemnn  12876  sqrt2irrap  12877  crth  12921  eulerthlemh  12928  prmdiveq  12933  powm2modprm  12950  modprm0  12952  pythagtriplem2  12964  pythagtriplem11  12972  pythagtriplem13  12974  pythagtrip  12981  pcid  13022  pcgcd1  13026  pcprmpw2  13031  dvdsprmpweqle  13035  pcaddlem  13037  pcadd  13038  fldivp1  13046  4sqlem12  13100  4sqlem14  13102  4sqlem15  13103  4sqlem16  13104  unennn  13148  ennnfonelemg  13154  ennnfonelemhf1o  13164  inffinp1  13180  isstructr  13227  setscomd  13253  imasbas  13520  imasplusg  13521  imasmulr  13522  subm0  13695  lssvancl1  14515  lssvnegcl  14524  lspprvacl  14561  lspsneli  14563  lspsn  14564  znf1o  14799  ntrin  14989  topssnei  15027  restbasg  15033  cnntri  15089  txcn  15140  txlm  15144  cnmpt2res  15162  psmetlecl  15199  xmetlecl  15232  bldisj  15266  bdmet  15367  bdbl  15368  bdmopn  15369  xmetxp  15372  metcnp  15377  tgioo  15419  cncfmet  15457  dedekindeulemlub  15485  suplociccreex  15489  ellimc3apf  15525  limcimolemlt  15529  limccnp2cntop  15542  dvfvalap  15546  dvidsslem  15558  dvmulxxbr  15567  dvaddxx  15568  dvmulxx  15569  dviaddf  15570  dvimulf  15571  dvcoapbr  15572  dvmptclx  15583  cxplt3  15785  cxpltd  15793  cxpled  15794  cxplt3d  15800  cxple3d  15801  logbrec  15825  logbgcd1irraplemap  15834  pellexlem1  15845  pellexlem2  15846  wilthlem1  15848  mpodvdsmulf1o  15858  lgslem1  15873  lgslem3  15875  lgsdirprm  15907  gausslemma2dlem1f1o  15933  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquad2lem1  15954  lgsquad3  15957  m1lgs  15958  2lgslem1a1  15959  2sqlem7  15994  usgredg2v  16219  vtxd0nedgbfi  16294  clwwlknonex2  16434  gsumgfsumlem  16865  gfsump1  16868