Theorem syl22anc 1185

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 302	. 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 1182	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  f1oprg  5343  tfrexlem  6161  th3qlem1  6461  ssenen  6674  phplem4dom  6685  phplem4on  6690  fiunsnnn  6704  findcard2sd  6715  unsnfi  6736  sbthlemi9  6781  endjusym  6896  endjudisj  6970  djuen  6971  ltanqg  7109  ltmnqg  7110  ltnnnq  7132  addcmpblnq0  7152  addlocprlemeqgt  7241  distrlem1prl  7291  distrlem1pru  7292  distrlem4prl  7293  distrlem4pru  7294  addcanprleml  7323  recexprlem1ssl  7342  caucvgprlemloc  7384  caucvgprprlemloccalc  7393  mulcmpblnr  7437  ltasrg  7466  recexgt0sr  7469  mulextsr1lem  7475  mulextsr1  7476  srpospr  7478  prsrlt  7482  pitonnlem1p1  7533  recidpirq  7545  axpre-ltadd  7571  mulgt0d  7756  mul4d  7788  add4d  7802  add42d  7803  subcan  7888  addsub4d  7991  subadd4d  7992  sub4d  7993  2addsubd  7994  addsubeq4d  7995  muladdd  8045  mulsubd  8046  addgegt0d  8148  addge0d  8150  le2addd  8191  le2subd  8192  ltleaddd  8193  leltaddd  8194  lt2subd  8196  apreap  8215  apsym  8234  apcotr  8235  apadd1  8236  apneg  8239  mulext1  8240  mulap0r  8243  mulge0d  8249  mulap0d  8280  divdivdivap  8334  divcanap5  8335  divap0d  8427  recdivapd  8428  recdivap2d  8429  divcanap6d  8430  ddcanapd  8431  rec11apd  8432  divmuldivapd  8453  prodgt0  8468  lt2msq  8502  ledivdiv  8506  lediv12a  8510  recreclt  8516  divgt0d  8551  mulgt1d  8552  lemulge11d  8553  lemulge12d  8554  ltmul12ad  8557  lemul12ad  8558  lemul12bd  8559  nndivtr  8620  qreccl  9284  ledivdivd  9356  lediv12ad  9390  lt2mul2divd  9393  xlt2add  9504  xleaddadd  9511  iccss2  9568  iccssico2  9571  lincmb01cmp  9627  iccf1o  9628  fzrev2i  9707  qtri3or  9861  2tnp1ge0ge0  9915  modqid  9963  q0mod  9969  q1mod  9970  modqabs  9971  modqadd1  9975  mulqaddmodid  9978  mulp1mod1  9979  modqmuladd  9980  modqmuladdnn0  9982  qnegmod  9983  m1modnnsub1  9984  addmodid  9986  modqm1p1mod0  9989  modqltm1p1mod  9990  modqmul1  9991  q2submod  9999  modifeq2int  10000  modaddmodup  10001  modaddmodlo  10002  modqaddmulmod  10005  modqsubdir  10007  modqeqmodmin  10008  modsumfzodifsn  10010  addmodlteq  10012  frecfzennn  10040  ser3mono  10092  expcl2lemap  10146  mulexpzap  10174  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  ltexp2a  10186  leexp2a  10187  sqdivap  10198  expnbnd  10256  expsubapd  10276  lt2sqd  10296  le2sqd  10297  sq11d  10298  bcp1nk  10349  hashunlem  10391  zfz1isolem1  10424  cjap  10519  resqrexlem1arp  10617  resqrexlemp1rp  10618  resqrexlemglsq  10634  abs00ap  10674  absext  10675  absexpzap  10692  absrele  10695  sqrtmuld  10781  sqrtsq2d  10782  sqrtled  10783  sqrtltd  10784  sqr11d  10785  abs3lemd  10813  minmax  10840  xrmaxiflemlub  10856  xrltmaxsup  10865  xrminmax  10873  xrbdtri  10884  climuni  10901  2clim  10909  addcn2  10918  mulcn2  10920  fsum3  10995  mptfzshft  11050  fsumrev  11051  fisum0diag2  11055  modfsummodlemstep  11065  binomlem  11091  mertenslemi1  11143  efcllemp  11162  dvds1  11346  dvdsext  11348  mulmoddvds  11356  oexpneg  11369  evennn02n  11374  evennn2n  11375  bezoutlemmo  11487  mulgcd  11497  dvdssqlem  11511  rpmulgcd2  11569  isprm6  11618  sqrt2irraplemnn  11649  sqrt2irrap  11650  crth  11692  unennn  11702  ennnfonelemg  11708  ennnfonelemhf1o  11718  inffinp1  11734  isstructr  11756  ntrin  12075  topssnei  12113  restbasg  12119  cnntri  12174  txcn  12225  txlm  12229  cnmpt2res  12247  psmetlecl  12262  xmetlecl  12295  bldisj  12329  bdmet  12430  bdbl  12431  bdmopn  12432  metcnp  12436  tgioo  12465  cncfmet  12492  ellimc3ap  12511  limcimolemlt  12513  dvfvalap  12523