Theorem syl22anc 1217

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 304	. 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 1214	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  f1oprg  5411  tfrexlem  6231  th3qlem1  6531  enpr2d  6711  ssenen  6745  phplem4dom  6756  phplem4on  6761  fiunsnnn  6775  findcard2sd  6786  unsnfi  6807  sbthlemi9  6853  endjusym  6981  endjudisj  7066  djuen  7067  ltanqg  7208  ltmnqg  7209  ltnnnq  7231  addcmpblnq0  7251  addlocprlemeqgt  7340  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  addcanprleml  7422  recexprlem1ssl  7441  caucvgprlemloc  7483  caucvgprprlemloccalc  7492  mulcmpblnr  7549  ltasrg  7578  recexgt0sr  7581  mulextsr1lem  7588  mulextsr1  7589  srpospr  7591  prsrlt  7595  ltpsrprg  7611  mappsrprg  7612  pitonnlem1p1  7654  recidpirq  7666  axpre-ltadd  7694  mulgt0d  7885  mul4d  7917  add4d  7931  add42d  7932  subcan  8017  addsub4d  8120  subadd4d  8121  sub4d  8122  2addsubd  8123  addsubeq4d  8124  muladdd  8178  mulsubd  8179  addgegt0d  8281  addgtge0d  8282  addge0d  8284  le2addd  8325  le2subd  8326  ltleaddd  8327  leltaddd  8328  lt2subd  8330  apreap  8349  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  mulap0r  8377  mulge0d  8383  mulap0d  8419  divdivdivap  8473  divcanap5  8474  divap0d  8566  recdivapd  8567  recdivap2d  8568  divcanap6d  8569  ddcanapd  8570  rec11apd  8571  divmuldivapd  8592  subrecapd  8600  prodgt0  8610  lt2msq  8644  ledivdiv  8648  lediv12a  8652  recreclt  8658  divgt0d  8693  mulgt1d  8694  lemulge11d  8695  lemulge12d  8696  ltmul12ad  8699  lemul12ad  8700  lemul12bd  8701  nndivtr  8762  qreccl  9434  ledivdivd  9509  lediv12ad  9543  lt2mul2divd  9552  xlt2add  9663  xleaddadd  9670  iccss2  9727  iccssico2  9730  lincmb01cmp  9786  iccf1o  9787  fzrev2i  9866  qtri3or  10020  2tnp1ge0ge0  10074  modqid  10122  q0mod  10128  q1mod  10129  modqabs  10130  modqadd1  10134  mulqaddmodid  10137  mulp1mod1  10138  modqmuladd  10139  modqmuladdnn0  10141  qnegmod  10142  m1modnnsub1  10143  addmodid  10145  modqm1p1mod0  10148  modqltm1p1mod  10149  modqmul1  10150  q2submod  10158  modifeq2int  10159  modaddmodup  10160  modaddmodlo  10161  modqaddmulmod  10164  modqsubdir  10166  modqeqmodmin  10167  modsumfzodifsn  10169  addmodlteq  10171  frecfzennn  10199  ser3mono  10251  expcl2lemap  10305  mulexpzap  10333  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  ltexp2a  10345  leexp2a  10346  sqdivap  10357  expnbnd  10415  expsubapd  10435  lt2sqd  10455  le2sqd  10456  sq11d  10457  bcp1nk  10508  hashunlem  10550  zfz1isolem1  10583  cjap  10678  cnreim  10750  resqrexlem1arp  10777  resqrexlemp1rp  10778  resqrexlemglsq  10794  abs00ap  10834  absext  10835  absexpzap  10852  absrele  10855  sqrtmuld  10941  sqrtsq2d  10942  sqrtled  10943  sqrtltd  10944  sqr11d  10945  abs3lemd  10973  minmax  11001  xrmaxiflemlub  11017  xrltmaxsup  11026  xrminmax  11034  xrbdtri  11045  climuni  11062  2clim  11070  addcn2  11079  mulcn2  11081  fsum3  11156  mptfzshft  11211  fsumrev  11212  fisum0diag2  11216  modfsummodlemstep  11226  binomlem  11252  mertenslemi1  11304  efcllemp  11364  dvds1  11551  dvdsext  11553  mulmoddvds  11561  oexpneg  11574  evennn02n  11579  evennn2n  11580  bezoutlemmo  11694  mulgcd  11704  dvdssqlem  11718  rpmulgcd2  11776  isprm6  11825  sqrt2irraplemnn  11857  sqrt2irrap  11858  crth  11900  unennn  11910  ennnfonelemg  11916  ennnfonelemhf1o  11926  inffinp1  11942  isstructr  11974  ntrin  12293  topssnei  12331  restbasg  12337  cnntri  12393  txcn  12444  txlm  12448  cnmpt2res  12466  psmetlecl  12503  xmetlecl  12536  bldisj  12570  bdmet  12671  bdbl  12672  bdmopn  12673  xmetxp  12676  metcnp  12681  tgioo  12715  cncfmet  12748  dedekindeulemlub  12767  suplociccreex  12771  ellimc3apf  12798  limcimolemlt  12802  limccnp2cntop  12815  dvfvalap  12819  dvmulxxbr  12835  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvcoapbr  12840  dvmptclx  12849