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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  f1oprg  5688  tfrexlem  6610  th3qlem1  6916  en2prd  7112  enpr2d  7117  ssenen  7158  phplem4dom  7169  phplem4on  7175  fiunsnnn  7191  findcard2sd  7202  unsnfi  7232  sbthlemi9  7289  endjusym  7442  endjudisj  7572  djuen  7573  ltanqg  7773  ltmnqg  7774  ltnnnq  7796  addcmpblnq0  7816  addlocprlemeqgt  7905  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  addcanprleml  7987  recexprlem1ssl  8006  caucvgprlemloc  8048  caucvgprprlemloccalc  8057  mulcmpblnr  8114  ltasrg  8143  recexgt0sr  8146  mulextsr1lem  8153  mulextsr1  8154  srpospr  8156  prsrlt  8160  ltpsrprg  8176  mappsrprg  8177  pitonnlem1p1  8219  recidpirq  8231  axpre-ltadd  8259  mulgt0d  8456  mul4d  8488  add4d  8502  add42d  8503  subcan  8588  addsub4d  8691  subadd4d  8692  sub4d  8693  2addsubd  8694  addsubeq4d  8695  muladdd  8750  mulsubd  8751  addgegt0d  8854  addgtge0d  8855  addge0d  8857  le2addd  8899  le2subd  8900  ltleaddd  8901  leltaddd  8902  lt2subd  8904  apreap  8923  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulap0r  8951  mulge0d  8957  mulap0d  8994  divdivdivap  9051  divcanap5  9052  divap0d  9144  recdivapd  9145  recdivap2d  9146  divcanap6d  9147  ddcanapd  9148  rec11apd  9149  divmuldivapd  9170  divmuleqapd  9171  subrecapd  9179  prodgt0  9190  lt2msq  9224  ledivdiv  9228  lediv12a  9232  recreclt  9238  divgt0d  9273  mulgt1d  9274  lemulge11d  9275  lemulge12d  9276  ltmul12ad  9279  lemul12ad  9280  lemul12bd  9281  nndivtr  9355  qreccl  10057  ledivdivd  10139  lediv12ad  10173  lt2mul2divd  10182  xlt2add  10298  xleaddadd  10305  iccss2  10362  iccssico2  10365  lincmb01cmp  10421  iccf1o  10423  fzrev2i  10509  qtri3or  10691  elicore  10717  2tnp1ge0ge0  10756  modqid  10806  q0mod  10812  q1mod  10813  modqabs  10814  modqadd1  10818  mulqaddmodid  10821  mulp1mod1  10822  modqmuladd  10823  modqmuladdnn0  10825  qnegmod  10826  m1modnnsub1  10827  addmodid  10829  modqm1p1mod0  10832  modqltm1p1mod  10833  modqmul1  10834  q2submod  10842  modifeq2int  10843  modaddmodup  10844  modaddmodlo  10845  modqaddmulmod  10848  modqsubdir  10850  modqeqmodmin  10851  modsumfzodifsn  10853  addmodlteq  10855  frecfzennn  10883  ser3mono  10944  expcl2lemap  11008  mulexpzap  11036  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  ltexp2a  11048  leexp2a  11049  sqdivap  11060  qsqeqor  11107  expnbnd  11121  expsubapd  11142  lt2sqd  11162  le2sqd  11163  sq11d  11164  apexp1  11177  bcp1nk  11221  hashunlem  11265  hashf1lem1  11306  zfz1isolem1  11313  hashtpgim  11318  sq01  11681  cjap  11693  cnreim  11765  resqrexlem1arp  11792  resqrexlemp1rp  11793  resqrexlemglsq  11809  abs00ap  11849  absext  11850  absexpzap  11868  absrele  11871  sqrtmuld  11957  sqrtsq2d  11958  sqrtled  11959  sqrtltd  11960  sqr11d  11961  abs3lemd  11989  minmax  12019  xrmaxiflemlub  12038  xrltmaxsup  12047  xrminmax  12055  xrbdtri  12066  climuni  12083  2clim  12091  addcn2  12100  mulcn2  12102  fsum3  12178  mptfzshft  12233  fsumrev  12234  fisum0diag2  12238  modfsummodlemstep  12248  binomlem  12274  mertenslemi1  12326  fprodrev  12410  efcllemp  12449  p1modz1  12585  dvds1  12644  dvdsext  12646  mulmoddvds  12654  oexpneg  12668  evennn02n  12673  evennn2n  12674  bitsinv1  12753  bezoutlemmo  12807  mulgcd  12817  dvdssqlem  12831  rpmulgcd2  12897  isprm6  12950  sqrt2irraplemnn  12983  sqrt2irrap  12984  sqrtrirr  13013  crth  13030  eulerthlemh  13037  prmdiveq  13042  powm2modprm  13059  modprm0  13061  pythagtriplem2  13073  pythagtriplem11  13081  pythagtriplem13  13083  pythagtrip  13090  pcid  13131  pcgcd1  13135  pcprmpw2  13140  dvdsprmpweqle  13144  pcaddlem  13146  pcadd  13147  fldivp1  13155  4sqlem12  13209  4sqlem14  13211  4sqlem15  13212  4sqlem16  13213  ballotfilemsima  13316  ballotfilemfrceq  13329  unennn  13345  ennnfonelemg  13351  ennnfonelemhf1o  13361  inffinp1  13377  isstructr  13424  setscomd  13450  imasbas  13686  imasplusg  13687  imasmulr  13688  subm0  13847  gzsumshift  14238  gsump1  14246  lssvancl1  14812  lssvnegcl  14821  lspprvacl  14858  lspsneli  14860  lspsn  14861  znf1o  15094  ntrin  15367  topssnei  15405  restbasg  15411  cnntri  15467  txcn  15518  txlm  15522  cnmpt2res  15540  psmetlecl  15577  xmetlecl  15610  bldisj  15644  bdmet  15745  bdbl  15746  bdmopn  15747  xmetxp  15750  metcnp  15755  tgioo  15797  cncfmet  15835  dedekindeulemlub  15863  suplociccreex  15867  ellimc3apf  15903  limcimolemlt  15907  limccnp2cntop  15920  dvfvalap  15924  dvidsslem  15936  dvmulxxbr  15945  dvaddxx  15946  dvmulxx  15947  dviaddf  15948  dvimulf  15949  dvcoapbr  15950  dvmptclx  15961  rpcxpmul2z  16165  cxplt3  16172  cxpltd  16180  cxpled  16181  cxplt3d  16187  cxple3d  16188  logbrec  16213  logbgcd1irraplemap  16222  zprmlogbaplem1  16232  log2tlbndlog2  16237  birthdaylem3  16244  pellexlem1  16246  pellexlem2  16247  wilthlem1  16249  ppiqsval  16257  chtqwordi  16280  ppiqwordi  16285  mpodvdsmulf1o  16301  ppiqub  16310  bclbnd  16324  bposlem7  16334  lgslem1  16341  lgslem3  16343  lgsdirprm  16375  gausslemma2dlem1f1o  16401  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquad2lem1  16422  lgsquad3  16425  m1lgs  16426  2lgslem1a1  16427  2sqlem7  16462  usgredg2v  16687  vtxd0nedgbfi  16762  clwwlknonex2  16902