Theorem syl22anc 1250

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 1247	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  5548  tfrexlem  6392  th3qlem1  6696  enpr2d  6876  ssenen  6912  phplem4dom  6923  phplem4on  6928  fiunsnnn  6942  findcard2sd  6953  unsnfi  6980  sbthlemi9  7031  endjusym  7162  endjudisj  7277  djuen  7278  ltanqg  7467  ltmnqg  7468  ltnnnq  7490  addcmpblnq0  7510  addlocprlemeqgt  7599  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  addcanprleml  7681  recexprlem1ssl  7700  caucvgprlemloc  7742  caucvgprprlemloccalc  7751  mulcmpblnr  7808  ltasrg  7837  recexgt0sr  7840  mulextsr1lem  7847  mulextsr1  7848  srpospr  7850  prsrlt  7854  ltpsrprg  7870  mappsrprg  7871  pitonnlem1p1  7913  recidpirq  7925  axpre-ltadd  7953  mulgt0d  8149  mul4d  8181  add4d  8195  add42d  8196  subcan  8281  addsub4d  8384  subadd4d  8385  sub4d  8386  2addsubd  8387  addsubeq4d  8388  muladdd  8442  mulsubd  8443  addgegt0d  8546  addgtge0d  8547  addge0d  8549  le2addd  8590  le2subd  8591  ltleaddd  8592  leltaddd  8593  lt2subd  8595  apreap  8614  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  mulap0r  8642  mulge0d  8648  mulap0d  8685  divdivdivap  8740  divcanap5  8741  divap0d  8833  recdivapd  8834  recdivap2d  8835  divcanap6d  8836  ddcanapd  8837  rec11apd  8838  divmuldivapd  8859  divmuleqapd  8860  subrecapd  8868  prodgt0  8879  lt2msq  8913  ledivdiv  8917  lediv12a  8921  recreclt  8927  divgt0d  8962  mulgt1d  8963  lemulge11d  8964  lemulge12d  8965  ltmul12ad  8968  lemul12ad  8969  lemul12bd  8970  nndivtr  9032  qreccl  9716  ledivdivd  9797  lediv12ad  9831  lt2mul2divd  9840  xlt2add  9955  xleaddadd  9962  iccss2  10019  iccssico2  10022  lincmb01cmp  10078  iccf1o  10079  fzrev2i  10161  qtri3or  10330  elicore  10356  2tnp1ge0ge0  10391  modqid  10441  q0mod  10447  q1mod  10448  modqabs  10449  modqadd1  10453  mulqaddmodid  10456  mulp1mod1  10457  modqmuladd  10458  modqmuladdnn0  10460  qnegmod  10461  m1modnnsub1  10462  addmodid  10464  modqm1p1mod0  10467  modqltm1p1mod  10468  modqmul1  10469  q2submod  10477  modifeq2int  10478  modaddmodup  10479  modaddmodlo  10480  modqaddmulmod  10483  modqsubdir  10485  modqeqmodmin  10486  modsumfzodifsn  10488  addmodlteq  10490  frecfzennn  10518  ser3mono  10579  expcl2lemap  10643  mulexpzap  10671  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  ltexp2a  10683  leexp2a  10684  sqdivap  10695  qsqeqor  10742  expnbnd  10755  expsubapd  10776  lt2sqd  10796  le2sqd  10797  sq11d  10798  apexp1  10810  bcp1nk  10854  hashunlem  10896  zfz1isolem1  10932  cjap  11071  cnreim  11143  resqrexlem1arp  11170  resqrexlemp1rp  11171  resqrexlemglsq  11187  abs00ap  11227  absext  11228  absexpzap  11245  absrele  11248  sqrtmuld  11334  sqrtsq2d  11335  sqrtled  11336  sqrtltd  11337  sqr11d  11338  abs3lemd  11366  minmax  11395  xrmaxiflemlub  11413  xrltmaxsup  11422  xrminmax  11430  xrbdtri  11441  climuni  11458  2clim  11466  addcn2  11475  mulcn2  11477  fsum3  11552  mptfzshft  11607  fsumrev  11608  fisum0diag2  11612  modfsummodlemstep  11622  binomlem  11648  mertenslemi1  11700  fprodrev  11784  efcllemp  11823  p1modz1  11959  dvds1  12018  dvdsext  12020  mulmoddvds  12028  oexpneg  12042  evennn02n  12047  evennn2n  12048  bezoutlemmo  12173  mulgcd  12183  dvdssqlem  12197  rpmulgcd2  12263  isprm6  12315  sqrt2irraplemnn  12347  sqrt2irrap  12348  crth  12392  eulerthlemh  12399  prmdiveq  12404  powm2modprm  12421  modprm0  12423  pythagtriplem2  12435  pythagtriplem11  12443  pythagtriplem13  12445  pythagtrip  12452  pcid  12493  pcgcd1  12497  pcprmpw2  12502  dvdsprmpweqle  12506  pcaddlem  12508  pcadd  12509  fldivp1  12517  4sqlem12  12571  4sqlem14  12573  4sqlem15  12574  4sqlem16  12575  unennn  12614  ennnfonelemg  12620  ennnfonelemhf1o  12630  inffinp1  12646  isstructr  12693  setscomd  12719  imasbas  12950  imasplusg  12951  imasmulr  12952  subm0  13114  lssvancl1  13923  lssvnegcl  13932  lspprvacl  13969  lspsneli  13971  lspsn  13972  znf1o  14207  ntrin  14360  topssnei  14398  restbasg  14404  cnntri  14460  txcn  14511  txlm  14515  cnmpt2res  14533  psmetlecl  14570  xmetlecl  14603  bldisj  14637  bdmet  14738  bdbl  14739  bdmopn  14740  xmetxp  14743  metcnp  14748  tgioo  14790  cncfmet  14828  dedekindeulemlub  14856  suplociccreex  14860  ellimc3apf  14896  limcimolemlt  14900  limccnp2cntop  14913  dvfvalap  14917  dvidsslem  14929  dvmulxxbr  14938  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvcoapbr  14943  dvmptclx  14954  cxplt3  15156  cxpltd  15164  cxpled  15165  cxplt3d  15171  cxple3d  15172  logbrec  15196  logbgcd1irraplemap  15205  wilthlem1  15216  mpodvdsmulf1o  15226  lgslem1  15241  lgslem3  15243  lgsdirprm  15275  gausslemma2dlem1f1o  15301  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquad2lem1  15322  lgsquad3  15325  m1lgs  15326  2lgslem1a1  15327  2sqlem7  15362