Theorem syl22anc 1279

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 1276	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  5680  tfrexlem  6595  th3qlem1  6901  en2prd  7096  enpr2d  7101  ssenen  7142  phplem4dom  7153  phplem4on  7159  fiunsnnn  7175  findcard2sd  7186  unsnfi  7216  sbthlemi9  7272  fsuppcorn  7291  endjusym  7426  endjudisj  7556  djuen  7557  ltanqg  7757  ltmnqg  7758  ltnnnq  7780  addcmpblnq0  7800  addlocprlemeqgt  7889  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  addcanprleml  7971  recexprlem1ssl  7990  caucvgprlemloc  8032  caucvgprprlemloccalc  8041  mulcmpblnr  8098  ltasrg  8127  recexgt0sr  8130  mulextsr1lem  8137  mulextsr1  8138  srpospr  8140  prsrlt  8144  ltpsrprg  8160  mappsrprg  8161  pitonnlem1p1  8203  recidpirq  8215  axpre-ltadd  8243  mulgt0d  8439  mul4d  8471  add4d  8485  add42d  8486  subcan  8571  addsub4d  8674  subadd4d  8675  sub4d  8676  2addsubd  8677  addsubeq4d  8678  muladdd  8733  mulsubd  8734  addgegt0d  8837  addgtge0d  8838  addge0d  8840  le2addd  8881  le2subd  8882  ltleaddd  8883  leltaddd  8884  lt2subd  8886  apreap  8905  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  mulap0r  8933  mulge0d  8939  mulap0d  8976  divdivdivap  9033  divcanap5  9034  divap0d  9126  recdivapd  9127  recdivap2d  9128  divcanap6d  9129  ddcanapd  9130  rec11apd  9131  divmuldivapd  9152  divmuleqapd  9153  subrecapd  9161  prodgt0  9172  lt2msq  9206  ledivdiv  9210  lediv12a  9214  recreclt  9220  divgt0d  9255  mulgt1d  9256  lemulge11d  9257  lemulge12d  9258  ltmul12ad  9261  lemul12ad  9262  lemul12bd  9263  nndivtr  9325  qreccl  10021  ledivdivd  10102  lediv12ad  10136  lt2mul2divd  10145  xlt2add  10261  xleaddadd  10268  iccss2  10325  iccssico2  10328  lincmb01cmp  10384  iccf1o  10386  fzrev2i  10471  qtri3or  10653  elicore  10679  2tnp1ge0ge0  10714  modqid  10764  q0mod  10770  q1mod  10771  modqabs  10772  modqadd1  10776  mulqaddmodid  10779  mulp1mod1  10780  modqmuladd  10781  modqmuladdnn0  10783  qnegmod  10784  m1modnnsub1  10785  addmodid  10787  modqm1p1mod0  10790  modqltm1p1mod  10791  modqmul1  10792  q2submod  10800  modifeq2int  10801  modaddmodup  10802  modaddmodlo  10803  modqaddmulmod  10806  modqsubdir  10808  modqeqmodmin  10809  modsumfzodifsn  10811  addmodlteq  10813  frecfzennn  10841  ser3mono  10902  expcl2lemap  10966  mulexpzap  10994  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  ltexp2a  11006  leexp2a  11007  sqdivap  11018  qsqeqor  11065  expnbnd  11079  expsubapd  11100  lt2sqd  11120  le2sqd  11121  sq11d  11122  apexp1  11134  bcp1nk  11178  hashunlem  11222  hashf1lem1  11263  zfz1isolem1  11270  hashtpgim  11275  sq01  11638  cjap  11650  cnreim  11722  resqrexlem1arp  11749  resqrexlemp1rp  11750  resqrexlemglsq  11766  abs00ap  11806  absext  11807  absexpzap  11824  absrele  11827  sqrtmuld  11913  sqrtsq2d  11914  sqrtled  11915  sqrtltd  11916  sqr11d  11917  abs3lemd  11945  minmax  11974  xrmaxiflemlub  11992  xrltmaxsup  12001  xrminmax  12009  xrbdtri  12020  climuni  12037  2clim  12045  addcn2  12054  mulcn2  12056  fsum3  12132  mptfzshft  12187  fsumrev  12188  fisum0diag2  12192  modfsummodlemstep  12202  binomlem  12228  mertenslemi1  12280  fprodrev  12364  efcllemp  12403  p1modz1  12539  dvds1  12598  dvdsext  12600  mulmoddvds  12608  oexpneg  12622  evennn02n  12627  evennn2n  12628  bitsinv1  12707  bezoutlemmo  12761  mulgcd  12771  dvdssqlem  12785  rpmulgcd2  12851  isprm6  12903  sqrt2irraplemnn  12935  sqrt2irrap  12936  crth  12980  eulerthlemh  12987  prmdiveq  12992  powm2modprm  13009  modprm0  13011  pythagtriplem2  13023  pythagtriplem11  13031  pythagtriplem13  13033  pythagtrip  13040  pcid  13081  pcgcd1  13085  pcprmpw2  13090  dvdsprmpweqle  13094  pcaddlem  13096  pcadd  13097  fldivp1  13105  4sqlem12  13159  4sqlem14  13161  4sqlem15  13162  4sqlem16  13163  ballotfilemsima  13237  ballotfilemfrceq  13250  unennn  13266  ennnfonelemg  13272  ennnfonelemhf1o  13282  inffinp1  13298  isstructr  13345  setscomd  13371  imasbas  13605  imasplusg  13606  imasmulr  13607  subm0  13766  gzsumshift  14126  gsump1  14134  lssvancl1  14676  lssvnegcl  14685  lspprvacl  14722  lspsneli  14724  lspsn  14725  znf1o  14958  ntrin  15148  topssnei  15186  restbasg  15192  cnntri  15248  txcn  15299  txlm  15303  cnmpt2res  15321  psmetlecl  15358  xmetlecl  15391  bldisj  15425  bdmet  15526  bdbl  15527  bdmopn  15528  xmetxp  15531  metcnp  15536  tgioo  15578  cncfmet  15616  dedekindeulemlub  15644  suplociccreex  15648  ellimc3apf  15684  limcimolemlt  15688  limccnp2cntop  15701  dvfvalap  15705  dvidsslem  15717  dvmulxxbr  15726  dvaddxx  15727  dvmulxx  15728  dviaddf  15729  dvimulf  15730  dvcoapbr  15731  dvmptclx  15742  cxplt3  15945  cxpltd  15953  cxpled  15954  cxplt3d  15960  cxple3d  15961  logbrec  15985  logbgcd1irraplemap  15994  pellexlem1  16005  pellexlem2  16006  wilthlem1  16008  mpodvdsmulf1o  16018  lgslem1  16033  lgslem3  16035  lgsdirprm  16067  gausslemma2dlem1f1o  16093  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquad2lem1  16114  lgsquad3  16117  m1lgs  16118  2lgslem1a1  16119  2sqlem7  16154  usgredg2v  16379  vtxd0nedgbfi  16454  clwwlknonex2  16594