Theorem syl22anc 1272

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 1269	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  5625  tfrexlem  6495  th3qlem1  6801  en2prd  6987  enpr2d  6992  ssenen  7032  phplem4dom  7043  phplem4on  7049  fiunsnnn  7063  findcard2sd  7074  unsnfi  7104  sbthlemi9  7155  endjusym  7286  endjudisj  7415  djuen  7416  ltanqg  7610  ltmnqg  7611  ltnnnq  7633  addcmpblnq0  7653  addlocprlemeqgt  7742  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  addcanprleml  7824  recexprlem1ssl  7843  caucvgprlemloc  7885  caucvgprprlemloccalc  7894  mulcmpblnr  7951  ltasrg  7980  recexgt0sr  7983  mulextsr1lem  7990  mulextsr1  7991  srpospr  7993  prsrlt  7997  ltpsrprg  8013  mappsrprg  8014  pitonnlem1p1  8056  recidpirq  8068  axpre-ltadd  8096  mulgt0d  8292  mul4d  8324  add4d  8338  add42d  8339  subcan  8424  addsub4d  8527  subadd4d  8528  sub4d  8529  2addsubd  8530  addsubeq4d  8531  muladdd  8585  mulsubd  8586  addgegt0d  8689  addgtge0d  8690  addge0d  8692  le2addd  8733  le2subd  8734  ltleaddd  8735  leltaddd  8736  lt2subd  8738  apreap  8757  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  mulap0r  8785  mulge0d  8791  mulap0d  8828  divdivdivap  8883  divcanap5  8884  divap0d  8976  recdivapd  8977  recdivap2d  8978  divcanap6d  8979  ddcanapd  8980  rec11apd  8981  divmuldivapd  9002  divmuleqapd  9003  subrecapd  9011  prodgt0  9022  lt2msq  9056  ledivdiv  9060  lediv12a  9064  recreclt  9070  divgt0d  9105  mulgt1d  9106  lemulge11d  9107  lemulge12d  9108  ltmul12ad  9111  lemul12ad  9112  lemul12bd  9113  nndivtr  9175  qreccl  9866  ledivdivd  9947  lediv12ad  9981  lt2mul2divd  9990  xlt2add  10105  xleaddadd  10112  iccss2  10169  iccssico2  10172  lincmb01cmp  10228  iccf1o  10229  fzrev2i  10311  qtri3or  10490  elicore  10516  2tnp1ge0ge0  10551  modqid  10601  q0mod  10607  q1mod  10608  modqabs  10609  modqadd1  10613  mulqaddmodid  10616  mulp1mod1  10617  modqmuladd  10618  modqmuladdnn0  10620  qnegmod  10621  m1modnnsub1  10622  addmodid  10624  modqm1p1mod0  10627  modqltm1p1mod  10628  modqmul1  10629  q2submod  10637  modifeq2int  10638  modaddmodup  10639  modaddmodlo  10640  modqaddmulmod  10643  modqsubdir  10645  modqeqmodmin  10646  modsumfzodifsn  10648  addmodlteq  10650  frecfzennn  10678  ser3mono  10739  expcl2lemap  10803  mulexpzap  10831  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  ltexp2a  10843  leexp2a  10844  sqdivap  10855  qsqeqor  10902  expnbnd  10915  expsubapd  10936  lt2sqd  10956  le2sqd  10957  sq11d  10958  apexp1  10970  bcp1nk  11014  hashunlem  11057  zfz1isolem1  11094  cjap  11457  cnreim  11529  resqrexlem1arp  11556  resqrexlemp1rp  11557  resqrexlemglsq  11573  abs00ap  11613  absext  11614  absexpzap  11631  absrele  11634  sqrtmuld  11720  sqrtsq2d  11721  sqrtled  11722  sqrtltd  11723  sqr11d  11724  abs3lemd  11752  minmax  11781  xrmaxiflemlub  11799  xrltmaxsup  11808  xrminmax  11816  xrbdtri  11827  climuni  11844  2clim  11852  addcn2  11861  mulcn2  11863  fsum3  11938  mptfzshft  11993  fsumrev  11994  fisum0diag2  11998  modfsummodlemstep  12008  binomlem  12034  mertenslemi1  12086  fprodrev  12170  efcllemp  12209  p1modz1  12345  dvds1  12404  dvdsext  12406  mulmoddvds  12414  oexpneg  12428  evennn02n  12433  evennn2n  12434  bitsinv1  12513  bezoutlemmo  12567  mulgcd  12577  dvdssqlem  12591  rpmulgcd2  12657  isprm6  12709  sqrt2irraplemnn  12741  sqrt2irrap  12742  crth  12786  eulerthlemh  12793  prmdiveq  12798  powm2modprm  12815  modprm0  12817  pythagtriplem2  12829  pythagtriplem11  12837  pythagtriplem13  12839  pythagtrip  12846  pcid  12887  pcgcd1  12891  pcprmpw2  12896  dvdsprmpweqle  12900  pcaddlem  12902  pcadd  12903  fldivp1  12911  4sqlem12  12965  4sqlem14  12967  4sqlem15  12968  4sqlem16  12969  unennn  13008  ennnfonelemg  13014  ennnfonelemhf1o  13024  inffinp1  13040  isstructr  13087  setscomd  13113  imasbas  13380  imasplusg  13381  imasmulr  13382  subm0  13555  lssvancl1  14371  lssvnegcl  14380  lspprvacl  14417  lspsneli  14419  lspsn  14420  znf1o  14655  ntrin  14838  topssnei  14876  restbasg  14882  cnntri  14938  txcn  14989  txlm  14993  cnmpt2res  15011  psmetlecl  15048  xmetlecl  15081  bldisj  15115  bdmet  15216  bdbl  15217  bdmopn  15218  xmetxp  15221  metcnp  15226  tgioo  15268  cncfmet  15306  dedekindeulemlub  15334  suplociccreex  15338  ellimc3apf  15374  limcimolemlt  15378  limccnp2cntop  15391  dvfvalap  15395  dvidsslem  15407  dvmulxxbr  15416  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvcoapbr  15421  dvmptclx  15432  cxplt3  15634  cxpltd  15642  cxpled  15643  cxplt3d  15649  cxple3d  15650  logbrec  15674  logbgcd1irraplemap  15683  wilthlem1  15694  mpodvdsmulf1o  15704  lgslem1  15719  lgslem3  15721  lgsdirprm  15753  gausslemma2dlem1f1o  15779  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquad2lem1  15800  lgsquad3  15803  m1lgs  15804  2lgslem1a1  15805  2sqlem7  15840  usgredg2v  16063  vtxd0nedgbfi  16105  clwwlknonex2  16234