Theorem syl22anc 1279

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 1276	1 ⊢ (𝜑 → 𝜂)

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  6609  th3qlem1  6915  en2prd  7111  enpr2d  7116  ssenen  7157  phplem4dom  7168  phplem4on  7174  fiunsnnn  7190  findcard2sd  7201  unsnfi  7231  sbthlemi9  7288  fsuppcorn  7307  endjusym  7443  endjudisj  7573  djuen  7574  ltanqg  7774  ltmnqg  7775  ltnnnq  7797  addcmpblnq0  7817  addlocprlemeqgt  7906  distrlem1prl  7956  distrlem1pru  7957  distrlem4prl  7958  distrlem4pru  7959  addcanprleml  7988  recexprlem1ssl  8007  caucvgprlemloc  8049  caucvgprprlemloccalc  8058  mulcmpblnr  8115  ltasrg  8144  recexgt0sr  8147  mulextsr1lem  8154  mulextsr1  8155  srpospr  8157  prsrlt  8161  ltpsrprg  8177  mappsrprg  8178  pitonnlem1p1  8220  recidpirq  8232  axpre-ltadd  8260  mulgt0d  8457  mul4d  8489  add4d  8503  add42d  8504  subcan  8589  addsub4d  8692  subadd4d  8693  sub4d  8694  2addsubd  8695  addsubeq4d  8696  muladdd  8751  mulsubd  8752  addgegt0d  8855  addgtge0d  8856  addge0d  8858  le2addd  8900  le2subd  8901  ltleaddd  8902  leltaddd  8903  lt2subd  8905  apreap  8924  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  mulap0r  8952  mulge0d  8958  mulap0d  8995  divdivdivap  9052  divcanap5  9053  divap0d  9145  recdivapd  9146  recdivap2d  9147  divcanap6d  9148  ddcanapd  9149  rec11apd  9150  divmuldivapd  9171  divmuleqapd  9172  subrecapd  9180  prodgt0  9191  lt2msq  9225  ledivdiv  9229  lediv12a  9233  recreclt  9239  divgt0d  9274  mulgt1d  9275  lemulge11d  9276  lemulge12d  9277  ltmul12ad  9280  lemul12ad  9281  lemul12bd  9282  nndivtr  9356  qreccl  10059  ledivdivd  10141  lediv12ad  10175  lt2mul2divd  10184  xlt2add  10300  xleaddadd  10307  iccss2  10364  iccssico2  10367  lincmb01cmp  10423  iccf1o  10425  fzrev2i  10511  qtri3or  10693  elicore  10719  2tnp1ge0ge0  10758  modqid  10808  q0mod  10814  q1mod  10815  modqabs  10816  modqadd1  10820  mulqaddmodid  10823  mulp1mod1  10824  modqmuladd  10825  modqmuladdnn0  10827  qnegmod  10828  m1modnnsub1  10829  addmodid  10831  modqm1p1mod0  10834  modqltm1p1mod  10835  modqmul1  10836  q2submod  10844  modifeq2int  10845  modaddmodup  10846  modaddmodlo  10847  modqaddmulmod  10850  modqsubdir  10852  modqeqmodmin  10853  modsumfzodifsn  10855  addmodlteq  10857  frecfzennn  10885  ser3mono  10946  expcl2lemap  11010  mulexpzap  11038  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  ltexp2a  11050  leexp2a  11051  sqdivap  11062  qsqeqor  11109  expnbnd  11123  expsubapd  11144  lt2sqd  11164  le2sqd  11165  sq11d  11166  apexp1  11179  bcp1nk  11223  hashunlem  11267  hashf1lem1  11308  zfz1isolem1  11315  hashtpgim  11320  sq01  11683  cjap  11695  cnreim  11767  resqrexlem1arp  11794  resqrexlemp1rp  11795  resqrexlemglsq  11811  abs00ap  11851  absext  11852  absexpzap  11870  absrele  11873  sqrtmuld  11959  sqrtsq2d  11960  sqrtled  11961  sqrtltd  11962  sqr11d  11963  abs3lemd  11991  minmax  12021  xrmaxiflemlub  12040  xrltmaxsup  12049  xrminmax  12057  xrbdtri  12068  climuni  12085  2clim  12093  addcn2  12102  mulcn2  12104  fsum3  12180  mptfzshft  12235  fsumrev  12236  fisum0diag2  12240  modfsummodlemstep  12250  binomlem  12276  mertenslemi1  12328  fprodrev  12412  efcllemp  12451  p1modz1  12587  dvds1  12646  dvdsext  12648  mulmoddvds  12656  oexpneg  12670  evennn02n  12675  evennn2n  12676  bitsinv1  12755  bezoutlemmo  12809  mulgcd  12819  dvdssqlem  12833  rpmulgcd2  12899  isprm6  12952  sqrt2irraplemnn  12985  sqrt2irrap  12986  sqrtrirr  13015  crth  13032  eulerthlemh  13039  prmdiveq  13044  powm2modprm  13061  modprm0  13063  pythagtriplem2  13075  pythagtriplem11  13083  pythagtriplem13  13085  pythagtrip  13092  pcid  13133  pcgcd1  13137  pcprmpw2  13142  dvdsprmpweqle  13146  pcaddlem  13148  pcadd  13149  fldivp1  13157  4sqlem12  13211  4sqlem14  13213  4sqlem15  13214  4sqlem16  13215  ballotfilemsima  13318  ballotfilemfrceq  13331  unennn  13347  ennnfonelemg  13353  ennnfonelemhf1o  13363  inffinp1  13379  isstructr  13426  setscomd  13452  imasbas  13688  imasplusg  13689  imasmulr  13690  subm0  13849  gzsumshift  14240  gsump1  14248  lssvancl1  14814  lssvnegcl  14823  lspprvacl  14860  lspsneli  14862  lspsn  14863  znf1o  15096  ntrin  15362  topssnei  15400  restbasg  15406  cnntri  15462  txcn  15513  txlm  15517  cnmpt2res  15535  psmetlecl  15572  xmetlecl  15605  bldisj  15639  bdmet  15740  bdbl  15741  bdmopn  15742  xmetxp  15745  metcnp  15750  tgioo  15792  cncfmet  15830  dedekindeulemlub  15858  suplociccreex  15862  ellimc3apf  15898  limcimolemlt  15902  limccnp2cntop  15915  dvfvalap  15919  dvidsslem  15931  dvmulxxbr  15940  dvaddxx  15941  dvmulxx  15942  dviaddf  15943  dvimulf  15944  dvcoapbr  15945  dvmptclx  15956  rpcxpmul2z  16160  cxplt3  16167  cxpltd  16175  cxpled  16176  cxplt3d  16182  cxple3d  16183  logbrec  16208  logbgcd1irraplemap  16217  zprmlogbaplem1  16227  log2tlbndlog2  16232  birthdaylem3  16239  pellexlem1  16241  pellexlem2  16242  wilthlem1  16244  ppiqsval  16252  chtqwordi  16275  ppiqwordi  16280  mpodvdsmulf1o  16296  ppiqub  16305  bclbnd  16319  bposlem7  16329  lgslem1  16336  lgslem3  16338  lgsdirprm  16370  gausslemma2dlem1f1o  16396  gausslemma2dlem6  16403  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem4  16409  lgseisen  16410  lgsquadlem1  16413  lgsquad2lem1  16417  lgsquad3  16420  m1lgs  16421  2lgslem1a1  16422  2sqlem7  16457  usgredg2v  16682  vtxd0nedgbfi  16757  clwwlknonex2  16897