Theorem syl3anc 1227

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 )
syl111anc.4	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3anc	|- ( ph -> ta )

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1166	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl111anc.4	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
6	4, 5	syl 14	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   /\ w3a 967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  syl112anc  1231  syl121anc  1232  syl211anc  1233  syl113anc  1239  syl131anc  1240  syl311anc  1241  syld3an3  1272  3jaod  1293  mpd3an23  1328  stoic4a  1419  rspc3ev  2842  sbciedf  2981  euotd  4226  ordelord  4353  wetriext  4548  releldm  4833  relelrn  4834  f1imass  5736  ovmpodxf  5958  ovmpodf  5964  fovrnd  5977  offval  6051  caoftrn  6069  offval3  6094  fnmpoovd  6174  tfrlemisucaccv  6284  tfrlemiubacc  6289  tfr1onlemsucaccv  6300  tfr1onlembfn  6303  tfrcllemsucaccv  6313  tfrcllembfn  6316  rdgss  6342  rdgisuc1  6343  rdgisucinc  6344  frecrdg  6367  mapsspm  6639  en2d  6725  en3d  6726  dom3d  6731  ssdomg  6735  f1imaen2g  6750  2dom  6762  cnven  6765  mapen  6803  mapxpen  6805  phpelm  6823  fidifsnen  6827  dif1en  6836  dif1enen  6837  diffisn  6850  isinfinf  6854  unfidisj  6878  unfiin  6882  tpfidisj  6884  xpfi  6886  fisseneq  6888  phpeqd  6889  ssfirab  6890  fnfi  6893  f1dmvrnfibi  6900  iunfidisj  6902  f1finf1o  6903  en1eqsn  6904  fidcenumlemr  6911  updjudhcoinlf  7036  updjudhcoinrg  7037  difinfinf  7057  en2eleq  7142  en2other2  7143  dju1en  7160  djuassen  7164  xpdjuen  7165  addcmpblnq  7299  addassnqg  7314  distrnqg  7319  ltsonq  7330  ltanqg  7332  ltmnqg  7333  ltaddnq  7339  ltexnqq  7340  prarloclemarch  7350  ltrnqg  7352  addcmpblnq0  7375  nnanq0  7390  distrnq0  7391  addassnq0  7394  prarloclemlt  7425  prarloclemcalc  7434  addnqprllem  7459  addnqprulem  7460  addnqprl  7461  addnqpru  7462  addlocprlemgt  7466  appdivnq  7495  prmuloclemcalc  7497  mulnqprl  7500  mulnqpru  7501  mullocprlem  7502  distrlem4prl  7516  distrlem4pru  7517  ltprordil  7521  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemloc  7539  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  ltaprlem  7550  ltaprg  7551  addextpr  7553  recexprlem1ssu  7566  aptipr  7573  ltmprr  7574  caucvgprlemcanl  7576  cauappcvgprlemopl  7578  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemloc  7607  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprprlemloccalc  7616  caucvgprprlemml  7626  caucvgprprlemopl  7629  caucvgprprlemloc  7635  caucvgprprlemexb  7639  caucvgprprlemaddq  7640  caucvgprprlem1  7641  caucvgprprlem2  7642  suplocexprlemmu  7650  suplocexprlemru  7651  addcmpblnr  7671  mulcmpblnrlemg  7672  mulcmpblnr  7673  ltsrprg  7679  distrsrg  7691  lttrsr  7694  ltsosr  7696  1idsr  7700  ltasrg  7702  recexgt0sr  7705  mulgt0sr  7710  mulextsr1lem  7712  srpospr  7715  prsradd  7718  prsrlt  7719  caucvgsrlemoffval  7728  caucvgsrlemoffgt1  7731  caucvgsrlemoffres  7732  caucvgsr  7734  ltpsrprg  7735  map2psrprg  7737  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  pitoregt0  7781  recidpirqlemcalc  7789  axmulass  7805  axdistr  7806  rereceu  7821  recriota  7822  addassd  7912  mulassd  7913  adddid  7914  adddird  7915  lelttr  7978  letrd  8013  lelttrd  8014  lttrd  8015  mul12d  8041  mul32d  8042  mul31d  8043  add12d  8056  add32d  8057  cnegexlem3  8066  addcand  8073  addcan2d  8074  pncan  8095  pncan3  8097  subcan2  8114  subsub2  8117  subsub4  8122  npncan3  8127  pnpcan  8128  pnncan  8130  addsub4  8132  subaddd  8218  subadd2d  8219  addsubassd  8220  addsubd  8221  subadd23d  8222  addsub12d  8223  npncand  8224  nppcand  8225  nppcan2d  8226  nppcan3d  8227  subsubd  8228  subsub2d  8229  subsub3d  8230  subsub4d  8231  sub32d  8232  nnncand  8233  nnncan1d  8234  nnncan2d  8235  npncan3d  8236  pnpcand  8237  pnpcan2d  8238  pnncand  8239  ppncand  8240  subcand  8241  subcan2d  8242  subcanad  8243  subcan2ad  8245  subdid  8303  subdird  8304  ltadd2  8308  ltadd2d  8310  ltletrd  8312  ltsubadd  8321  lesubadd  8323  ltaddsub  8325  leaddsub  8327  le2add  8333  lt2add  8334  ltleadd  8335  lesub1  8345  lesub2  8346  ltsub1  8347  ltsub2  8348  lt2sub  8349  le2sub  8350  subge0  8364  lesub0  8368  ltadd1d  8427  leadd1d  8428  leadd2d  8429  ltsubaddd  8430  lesubaddd  8431  ltsubadd2d  8432  lesubadd2d  8433  ltaddsubd  8434  ltaddsub2d  8435  leaddsub2d  8436  subled  8437  lesubd  8438  ltsub23d  8439  ltsub13d  8440  lesub1d  8441  lesub2d  8442  ltsub1d  8443  ltsub2d  8444  gt0add  8462  apcotr  8496  apadd1  8497  addext  8499  mulext1  8501  mulext  8503  gtapd  8526  leltapd  8528  mulap0  8542  mul0eqap  8558  divvalap  8561  divcanap2  8567  diveqap0  8569  divrecap  8575  divassap  8577  divmulassap  8582  divmulasscomap  8583  divdirap  8584  divcanap3  8585  div11ap  8587  rec11ap  8597  divmuldivap  8599  divdivdivap  8600  divmuleqap  8604  dmdcanap  8609  ddcanap  8613  divadddivap  8614  divsubdivap  8615  redivclap  8618  apmul1  8675  divclapd  8677  divcanap1d  8678  divcanap2d  8679  divrecapd  8680  divrecap2d  8681  divcanap3d  8682  divcanap4d  8683  diveqap0d  8684  diveqap1d  8685  diveqap1ad  8686  diveqap0ad  8687  divap0bd  8689  divnegapd  8690  divneg2apd  8691  div2negapd  8692  redivclapd  8722  div2subap  8724  ltmul12a  8746  lemul12b  8747  lt2mul2div  8765  ltdiv2  8773  ltdiv23  8778  avglt1  9086  avglt2  9087  lt2halvesd  9095  div4p1lem1div2  9101  zltp1le  9236  elz2  9253  zdivmul  9272  uztrn  9473  eluzsub  9486  uz3m2nn  9502  qaddcl  9564  elpq  9577  cnref1o  9579  ltdiv2d  9647  lediv2d  9648  divlt1lt  9651  divle1le  9652  ledivge1le  9653  ltmulgt11d  9659  ltmulgt12d  9660  gt0divd  9661  ge0divd  9662  rpgecld  9663  ltmul1d  9665  ltmul2d  9666  lemul1d  9667  lemul2d  9668  ltdiv1d  9669  lediv1d  9670  ltmuldivd  9671  ltmuldiv2d  9672  lemuldivd  9673  lemuldiv2d  9674  ltdivmuld  9675  ltdivmul2d  9676  ledivmuld  9677  ledivmul2d  9678  ltdiv23d  9684  lediv23d  9685  addlelt  9695  xrltso  9723  xrlelttr  9733  xrlttrd  9736  xrlelttrd  9737  xrltletrd  9738  xrletrd  9739  xrre3  9749  xleadd1  9802  xltadd1  9803  xle2add  9806  xlt2add  9807  xlesubadd  9810  xadd4d  9812  ixxss1  9831  ixxss2  9832  ixxss12  9833  iooshf  9879  icoshftf1o  9918  ioodisj  9920  zltaddlt1le  9934  fznlem  9966  fzdifsuc  10006  fzrev  10009  fzrevral2  10031  elfz0fzfz0  10051  elfzmlbp  10057  fzctr  10058  elfzole1  10080  elfzolt2  10081  fzoss2  10097  fzospliti  10101  fzo1fzo0n0  10108  elfzo0z  10109  fzofzim  10113  fzoaddel  10117  eluzgtdifelfzo  10122  elfzodifsumelfzo  10126  ssfzo12bi  10150  elfzonelfzo  10155  fvinim0ffz  10166  rebtwn2zlemstep  10178  rebtwn2z  10180  qbtwnxr  10183  flqge  10207  2tnp1ge0ge0  10226  intfracq  10245  flqdiv  10246  modqval  10249  modqcld  10253  modqmulnn  10267  zmodcl  10269  zmodfz  10271  modqid  10274  zmodid2  10277  modqabs  10282  modqcyc  10284  modqadd1  10286  modqaddabs  10287  modqaddmod  10288  mulp1mod1  10290  modqmuladd  10291  modqmuladdim  10292  modqmuladdnn0  10293  m1modnnsub1  10295  modqltm1p1mod  10301  modqmul1  10302  modqsubmod  10307  modqsubmodmod  10308  q2txmodxeq0  10309  modaddmodup  10312  modqmulmod  10314  modqaddmulmod  10316  modqdi  10317  modqsubdir  10318  addmodlteq  10323  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdgrcl  10335  frecuzrdgsuc  10339  frecuzrdgrclt  10340  frecuzrdgg  10341  frecuzrdgsuctlem  10348  frecfzen2  10352  seq3val  10383  seqvalcd  10384  seqf  10386  seq3p1  10387  seqovcd  10388  seqp1cd  10391  monoord  10401  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemmo  10417  iseqf1olemqk  10419  seq3f1olemqsumkj  10423  seq3f1olemstep  10426  expnnval  10448  expnegap0  10453  rpexpcl  10464  expnegzap  10479  expgt1  10483  mulexpzap  10485  exprecap  10486  expaddzaplem  10488  expaddzap  10489  expmul  10490  expmulzap  10491  expdivap  10496  ltexp2a  10497  leexp2a  10498  leexp2r  10499  leexp1a  10500  bernneq2  10565  bernneq3  10566  expnbnd  10567  expnlbnd  10568  expnlbnd2  10569  expaddd  10579  expmuld  10580  expclzapd  10582  expap0d  10583  expnegapd  10584  exprecapd  10585  expp1zapd  10586  expm1apd  10587  sqdivapd  10590  mulexpd  10592  expge0d  10595  expge1d  10596  sqoddm1div8  10597  reexpclzapd  10602  leexp2ad  10606  facwordi  10642  faclbnd3  10645  facavg  10648  bcval  10651  bccmpl  10656  bc0k  10658  bcval5  10665  bcpasc  10668  hashfiv01gt1  10684  hashunlem  10706  hashunsng  10709  fiprsshashgt1  10719  hashdifsn  10721  hashdifpr  10722  hashfz  10723  hashxp  10728  hashfacen  10735  zfz1isolemiso  10738  zfz1isolem1  10739  zfz1iso  10740  shftfvalg  10746  seq3shft  10766  mulreap  10792  cjreb  10794  cjap  10834  cnrecnv  10838  cjdivapd  10896  redivapd  10902  imdivapd  10903  resqrexlemdecn  10940  absexpzap  11008  abslt  11016  absle  11017  elicc4abs  11022  abs3lem  11039  fzomaxdiflem  11040  cau3lem  11042  amgm2  11046  abssubge0d  11104  abssuble0d  11105  absdifltd  11106  absdifled  11107  absdivapd  11123  abs3difd  11128  qdenre  11130  maxabslemlub  11135  rexanre  11148  rexico  11149  fimaxre2  11154  lemininf  11161  ltmininf  11162  rpmincl  11165  mul0inf  11168  xrmaxiflemlub  11175  xrmaxltsup  11185  xrmaxaddlem  11187  xrmaxadd  11188  xrltmininf  11197  xrlemininf  11198  xrminltinf  11199  xrminadd  11202  xrbdtri  11203  climshftlemg  11229  climshft2  11233  addcn2  11237  mulcn2  11239  reccn2ap  11240  cn1lem  11241  climadd  11253  climmul  11254  climsub  11255  climsqz  11262  climsqz2  11263  climrecvg1n  11275  climcvg1nlem  11276  fisumss  11319  fsumsplitsn  11337  sumpr  11340  fsumsplitsnun  11346  fsum2dlemstep  11361  fisumcom2  11365  fisum0diag2  11374  fsumconst  11381  modfsummodlemstep  11384  fsumlessfi  11387  fsumabs  11392  fsumiun  11404  hashiun  11405  hash2iun  11406  hash2iun1dif1  11407  binomlem  11410  bcxmas  11416  isumshft  11417  isumlessdc  11423  expcnvap0  11429  expcnvre  11430  geosergap  11433  cvgratnnlembern  11450  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  mertenslemi1  11462  fprodssdc  11517  fprodm1  11525  fprodunsn  11531  fprodeq0  11544  fprod2dlemstep  11549  fprodcom2fi  11553  fprodsplitsn  11560  fprodsplit1f  11561  efaddlem  11601  eftlub  11617  efltim  11625  eirraplem  11703  dvdsval3  11717  nndivdvds  11722  modm1div  11726  summodnegmod  11748  modmulconst  11749  dvds2subd  11753  dvdstrd  11755  dvdsmultr1d  11757  dvdsmultr2  11758  dvdsabseq  11770  dvdsfac  11783  dvdsmod  11785  oddge22np1  11803  ltoddhalfle  11815  halfleoddlt  11816  nn0ehalf  11825  nno  11828  nn0oddm1d2  11831  divalglemnn  11840  divalg  11846  divalgmod  11849  fldivndvdslt  11857  flodddiv4lt  11858  flodddiv4t2lthalf  11859  infssuzex  11867  dvdsbnd  11874  gcdneg  11900  gcdaddm  11902  modgcd  11909  gcdmultipled  11911  dvdsgcdidd  11912  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlembi  11923  dvdsgcdb  11931  gcdass  11933  mulgcd  11934  dvdsmulgcd  11943  rpmulgcd  11944  sqgcd  11947  nn0seqcvgd  11952  eucalglt  11968  gcddvdslcm  11984  lcmgcdlem  11988  lcmdvdsb  11995  lcmass  11996  ncoprmgcdne1b  12000  coprmdvds2  12004  mulgcddvds  12005  rpmulgcd2  12006  qredeu  12008  rpdvds  12010  divgcdcoprm0  12012  cncongr1  12014  cncongr2  12015  isprm2lem  12027  prmind2  12031  nprm  12034  dvdsnprmd  12036  exprmfct  12049  prmdvdsfz  12050  divgcdodd  12052  isprm6  12056  prmdvdsexp  12057  prmexpb  12060  prmfac1  12061  rpexp  12062  rpexp12i  12064  pw2dvdseulemle  12076  sqpweven  12084  2sqpwodd  12085  divnumden  12105  numdensq  12111  nonsq  12116  hashdvds  12130  phiprmpw  12131  crth  12133  phimullem  12134  eulerthlem1  12136  eulerthlemfi  12137  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  prmdiv  12144  prmdiveq  12145  prmdivdiv  12146  hashgcdlem  12147  phisum  12149  odzdvds  12154  odzphi  12155  vfermltl  12160  powm2modprm  12161  reumodprminv  12162  modprm0  12163  nnnn0modprm0  12164  modprmn0modprm0  12165  coprimeprodsq  12166  pythagtriplem4  12177  pythagtriplem19  12191  pclemub  12196  pcprendvds2  12200  pcpremul  12202  pcval  12205  pcdiv  12211  pcqdiv  12216  pcexp  12218  pcdvdsb  12228  pcidlem  12231  pcdvdstr  12235  pcgcd1  12236  pc2dvds  12238  pcprmpw2  12241  dvdsprmpweqle  12245  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmptdvds  12252  fldivp1  12255  pcfaclem  12256  pcfac  12257  pcbc  12258  oddprmdvds  12261  ennnfonelemp1  12276  ennnfonelemex  12284  ennnfonelemrn  12289  ctinfom  12298  ctiunct  12310  nninfdclemcl  12320  nninfdclemp1  12322  strsetsid  12364  fvsetsid  12365  setsabsd  12370  setscom  12371  ressid2  12390  ressval2  12391  srngstrd  12453  lmodstrd  12464  ipsstrd  12472  topgrpstrd  12482  difopn  12649  uncld  12654  ntrin  12665  clsss2  12670  ntrcls0  12672  topssnei  12703  neissex  12706  restbasg  12709  tgrest  12710  resttopon  12712  restabs  12716  restopnb  12722  cnpfval  12736  cnprcl2k  12747  tgcnp  12750  iscnp4  12759  cnpnei  12760  cnptopco  12763  cncnpi  12769  cncnp  12771  cnconst2  12774  cnrest  12776  cnrest2  12777  cnrest2r  12778  cnptopresti  12779  cnptoprest  12780  cnptoprest2  12781  lmss  12787  lmtopcnp  12791  txvalex  12795  txval  12796  txbasval  12808  txcnp  12812  txcnmpt  12814  txcn  12816  txdis1cn  12819  lmcn2  12821  cnmptc  12823  cnmpt11  12824  cnmpt1t  12826  cnmpt12  12828  cnmpt21  12832  cnmpt2t  12834  cnmpt22  12835  cnmpt22f  12836  cnmptcom  12839  hmeores  12856  txhmeo  12860  psmettri  12871  xmettri  12913  metrtri  12918  xmetres2  12920  blfvalps  12926  bldisj  12942  blgt0  12943  xblss2ps  12945  xblss2  12946  blhalf  12949  blininf  12965  blssps  12968  blss  12969  blssexps  12970  blssex  12971  blin2  12973  xmeter  12977  blnei  13033  blsscls2  13034  metss2lem  13038  bdmetval  13041  bdxmet  13042  bdbl  13044  xmetxp  13048  xmetxpbl  13049  xmettxlem  13050  xmettx  13051  metcnp3  13052  metcnp  13053  metcnp2  13054  metcnpi  13056  metcnpi2  13057  metcnpi3  13058  txmetcnp  13059  metcnpd  13061  tgqioo  13088  addcncntoplem  13092  fsumcncntop  13097  mulc1cncf  13117  cncfco  13119  mulcncflem  13131  mulcncf  13132  suplociccreex  13143  suplociccex  13144  dedekindicc  13152  ivthinclemlm  13153  ivthinclemum  13154  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthinclemloc  13160  ivthdec  13163  limccl  13169  ellimc3apf  13170  limcimolemlt  13174  cnplimclemle  13178  cnplimclemr  13179  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  reldvg  13189  eldvap  13192  dvbssntrcntop  13194  dvcnp2cntop  13204  dvmulxxbr  13207  dvrecap  13218  dveflem  13228  reeff1o  13235  efltlemlt  13236  sin0pilem2  13244  ptolemy  13286  sinq12gt0  13292  cxprec  13372  rpcxproot  13375  cxpmuld  13397  rpabscxpbnd  13400  rplogbval  13404  rplogbchbase  13409  relogbval  13410  relogbzcl  13411  rplogbreexp  13412  rprelogbmul  13414  rprelogbdiv  13416  nnlogbexp  13418  relogbcxpbap  13424  logbgt0b  13425  logbgcd1irr  13426  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  logbprmirr  13431  apdifflemr  13760  apdiff  13761  iswomni0  13764