Theorem syl22anc 1274

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl22anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl22anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylXanc.3	. 2 ⊢ (𝜑 → 𝜃)
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 1271	1 ⊢ (𝜑 → 𝜂)

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  5632  tfrexlem  6505  th3qlem1  6811  en2prd  6997  enpr2d  7002  ssenen  7042  phplem4dom  7053  phplem4on  7059  fiunsnnn  7075  findcard2sd  7086  unsnfi  7116  sbthlemi9  7169  endjusym  7300  endjudisj  7430  djuen  7431  ltanqg  7625  ltmnqg  7626  ltnnnq  7648  addcmpblnq0  7668  addlocprlemeqgt  7757  distrlem1prl  7807  distrlem1pru  7808  distrlem4prl  7809  distrlem4pru  7810  addcanprleml  7839  recexprlem1ssl  7858  caucvgprlemloc  7900  caucvgprprlemloccalc  7909  mulcmpblnr  7966  ltasrg  7995  recexgt0sr  7998  mulextsr1lem  8005  mulextsr1  8006  srpospr  8008  prsrlt  8012  ltpsrprg  8028  mappsrprg  8029  pitonnlem1p1  8071  recidpirq  8083  axpre-ltadd  8111  mulgt0d  8307  mul4d  8339  add4d  8353  add42d  8354  subcan  8439  addsub4d  8542  subadd4d  8543  sub4d  8544  2addsubd  8545  addsubeq4d  8546  muladdd  8600  mulsubd  8601  addgegt0d  8704  addgtge0d  8705  addge0d  8707  le2addd  8748  le2subd  8749  ltleaddd  8750  leltaddd  8751  lt2subd  8753  apreap  8772  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  mulap0r  8800  mulge0d  8806  mulap0d  8843  divdivdivap  8898  divcanap5  8899  divap0d  8991  recdivapd  8992  recdivap2d  8993  divcanap6d  8994  ddcanapd  8995  rec11apd  8996  divmuldivapd  9017  divmuleqapd  9018  subrecapd  9026  prodgt0  9037  lt2msq  9071  ledivdiv  9075  lediv12a  9079  recreclt  9085  divgt0d  9120  mulgt1d  9121  lemulge11d  9122  lemulge12d  9123  ltmul12ad  9126  lemul12ad  9127  lemul12bd  9128  nndivtr  9190  qreccl  9881  ledivdivd  9962  lediv12ad  9996  lt2mul2divd  10005  xlt2add  10120  xleaddadd  10127  iccss2  10184  iccssico2  10187  lincmb01cmp  10243  iccf1o  10244  fzrev2i  10326  qtri3or  10506  elicore  10532  2tnp1ge0ge0  10567  modqid  10617  q0mod  10623  q1mod  10624  modqabs  10625  modqadd1  10629  mulqaddmodid  10632  mulp1mod1  10633  modqmuladd  10634  modqmuladdnn0  10636  qnegmod  10637  m1modnnsub1  10638  addmodid  10640  modqm1p1mod0  10643  modqltm1p1mod  10644  modqmul1  10645  q2submod  10653  modifeq2int  10654  modaddmodup  10655  modaddmodlo  10656  modqaddmulmod  10659  modqsubdir  10661  modqeqmodmin  10662  modsumfzodifsn  10664  addmodlteq  10666  frecfzennn  10694  ser3mono  10755  expcl2lemap  10819  mulexpzap  10847  expaddzaplem  10850  expaddzap  10851  expmulzap  10853  ltexp2a  10859  leexp2a  10860  sqdivap  10871  qsqeqor  10918  expnbnd  10931  expsubapd  10952  lt2sqd  10972  le2sqd  10973  sq11d  10974  apexp1  10986  bcp1nk  11030  hashunlem  11073  zfz1isolem1  11110  hashtpgim  11115  cjap  11489  cnreim  11561  resqrexlem1arp  11588  resqrexlemp1rp  11589  resqrexlemglsq  11605  abs00ap  11645  absext  11646  absexpzap  11663  absrele  11666  sqrtmuld  11752  sqrtsq2d  11753  sqrtled  11754  sqrtltd  11755  sqr11d  11756  abs3lemd  11784  minmax  11813  xrmaxiflemlub  11831  xrltmaxsup  11840  xrminmax  11848  xrbdtri  11859  climuni  11876  2clim  11884  addcn2  11893  mulcn2  11895  fsum3  11971  mptfzshft  12026  fsumrev  12027  fisum0diag2  12031  modfsummodlemstep  12041  binomlem  12067  mertenslemi1  12119  fprodrev  12203  efcllemp  12242  p1modz1  12378  dvds1  12437  dvdsext  12439  mulmoddvds  12447  oexpneg  12461  evennn02n  12466  evennn2n  12467  bitsinv1  12546  bezoutlemmo  12600  mulgcd  12610  dvdssqlem  12624  rpmulgcd2  12690  isprm6  12742  sqrt2irraplemnn  12774  sqrt2irrap  12775  crth  12819  eulerthlemh  12826  prmdiveq  12831  powm2modprm  12848  modprm0  12850  pythagtriplem2  12862  pythagtriplem11  12870  pythagtriplem13  12872  pythagtrip  12879  pcid  12920  pcgcd1  12924  pcprmpw2  12929  dvdsprmpweqle  12933  pcaddlem  12935  pcadd  12936  fldivp1  12944  4sqlem12  12998  4sqlem14  13000  4sqlem15  13001  4sqlem16  13002  unennn  13041  ennnfonelemg  13047  ennnfonelemhf1o  13057  inffinp1  13073  isstructr  13120  setscomd  13146  imasbas  13413  imasplusg  13414  imasmulr  13415  subm0  13588  lssvancl1  14405  lssvnegcl  14414  lspprvacl  14451  lspsneli  14453  lspsn  14454  znf1o  14689  ntrin  14877  topssnei  14915  restbasg  14921  cnntri  14977  txcn  15028  txlm  15032  cnmpt2res  15050  psmetlecl  15087  xmetlecl  15120  bldisj  15154  bdmet  15255  bdbl  15256  bdmopn  15257  xmetxp  15260  metcnp  15265  tgioo  15307  cncfmet  15345  dedekindeulemlub  15373  suplociccreex  15377  ellimc3apf  15413  limcimolemlt  15417  limccnp2cntop  15430  dvfvalap  15434  dvidsslem  15446  dvmulxxbr  15455  dvaddxx  15456  dvmulxx  15457  dviaddf  15458  dvimulf  15459  dvcoapbr  15460  dvmptclx  15471  cxplt3  15673  cxpltd  15681  cxpled  15682  cxplt3d  15688  cxple3d  15689  logbrec  15713  logbgcd1irraplemap  15722  wilthlem1  15733  mpodvdsmulf1o  15743  lgslem1  15758  lgslem3  15760  lgsdirprm  15792  gausslemma2dlem1f1o  15818  gausslemma2dlem6  15825  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem4  15831  lgseisen  15832  lgsquadlem1  15835  lgsquad2lem1  15839  lgsquad3  15842  m1lgs  15843  2lgslem1a1  15844  2sqlem7  15879  usgredg2v  16104  vtxd0nedgbfi  16179  clwwlknonex2  16319  gsumgfsumlem  16751  gfsump1  16754