Theorem syl22anc 1272

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 1269	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  5625  tfrexlem  6495  th3qlem1  6801  en2prd  6987  enpr2d  6992  ssenen  7032  phplem4dom  7043  phplem4on  7049  fiunsnnn  7065  findcard2sd  7076  unsnfi  7106  sbthlemi9  7158  endjusym  7289  endjudisj  7418  djuen  7419  ltanqg  7613  ltmnqg  7614  ltnnnq  7636  addcmpblnq0  7656  addlocprlemeqgt  7745  distrlem1prl  7795  distrlem1pru  7796  distrlem4prl  7797  distrlem4pru  7798  addcanprleml  7827  recexprlem1ssl  7846  caucvgprlemloc  7888  caucvgprprlemloccalc  7897  mulcmpblnr  7954  ltasrg  7983  recexgt0sr  7986  mulextsr1lem  7993  mulextsr1  7994  srpospr  7996  prsrlt  8000  ltpsrprg  8016  mappsrprg  8017  pitonnlem1p1  8059  recidpirq  8071  axpre-ltadd  8099  mulgt0d  8295  mul4d  8327  add4d  8341  add42d  8342  subcan  8427  addsub4d  8530  subadd4d  8531  sub4d  8532  2addsubd  8533  addsubeq4d  8534  muladdd  8588  mulsubd  8589  addgegt0d  8692  addgtge0d  8693  addge0d  8695  le2addd  8736  le2subd  8737  ltleaddd  8738  leltaddd  8739  lt2subd  8741  apreap  8760  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  mulap0r  8788  mulge0d  8794  mulap0d  8831  divdivdivap  8886  divcanap5  8887  divap0d  8979  recdivapd  8980  recdivap2d  8981  divcanap6d  8982  ddcanapd  8983  rec11apd  8984  divmuldivapd  9005  divmuleqapd  9006  subrecapd  9014  prodgt0  9025  lt2msq  9059  ledivdiv  9063  lediv12a  9067  recreclt  9073  divgt0d  9108  mulgt1d  9109  lemulge11d  9110  lemulge12d  9111  ltmul12ad  9114  lemul12ad  9115  lemul12bd  9116  nndivtr  9178  qreccl  9869  ledivdivd  9950  lediv12ad  9984  lt2mul2divd  9993  xlt2add  10108  xleaddadd  10115  iccss2  10172  iccssico2  10175  lincmb01cmp  10231  iccf1o  10232  fzrev2i  10314  qtri3or  10493  elicore  10519  2tnp1ge0ge0  10554  modqid  10604  q0mod  10610  q1mod  10611  modqabs  10612  modqadd1  10616  mulqaddmodid  10619  mulp1mod1  10620  modqmuladd  10621  modqmuladdnn0  10623  qnegmod  10624  m1modnnsub1  10625  addmodid  10627  modqm1p1mod0  10630  modqltm1p1mod  10631  modqmul1  10632  q2submod  10640  modifeq2int  10641  modaddmodup  10642  modaddmodlo  10643  modqaddmulmod  10646  modqsubdir  10648  modqeqmodmin  10649  modsumfzodifsn  10651  addmodlteq  10653  frecfzennn  10681  ser3mono  10742  expcl2lemap  10806  mulexpzap  10834  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  ltexp2a  10846  leexp2a  10847  sqdivap  10858  qsqeqor  10905  expnbnd  10918  expsubapd  10939  lt2sqd  10959  le2sqd  10960  sq11d  10961  apexp1  10973  bcp1nk  11017  hashunlem  11060  zfz1isolem1  11097  cjap  11460  cnreim  11532  resqrexlem1arp  11559  resqrexlemp1rp  11560  resqrexlemglsq  11576  abs00ap  11616  absext  11617  absexpzap  11634  absrele  11637  sqrtmuld  11723  sqrtsq2d  11724  sqrtled  11725  sqrtltd  11726  sqr11d  11727  abs3lemd  11755  minmax  11784  xrmaxiflemlub  11802  xrltmaxsup  11811  xrminmax  11819  xrbdtri  11830  climuni  11847  2clim  11855  addcn2  11864  mulcn2  11866  fsum3  11941  mptfzshft  11996  fsumrev  11997  fisum0diag2  12001  modfsummodlemstep  12011  binomlem  12037  mertenslemi1  12089  fprodrev  12173  efcllemp  12212  p1modz1  12348  dvds1  12407  dvdsext  12409  mulmoddvds  12417  oexpneg  12431  evennn02n  12436  evennn2n  12437  bitsinv1  12516  bezoutlemmo  12570  mulgcd  12580  dvdssqlem  12594  rpmulgcd2  12660  isprm6  12712  sqrt2irraplemnn  12744  sqrt2irrap  12745  crth  12789  eulerthlemh  12796  prmdiveq  12801  powm2modprm  12818  modprm0  12820  pythagtriplem2  12832  pythagtriplem11  12840  pythagtriplem13  12842  pythagtrip  12849  pcid  12890  pcgcd1  12894  pcprmpw2  12899  dvdsprmpweqle  12903  pcaddlem  12905  pcadd  12906  fldivp1  12914  4sqlem12  12968  4sqlem14  12970  4sqlem15  12971  4sqlem16  12972  unennn  13011  ennnfonelemg  13017  ennnfonelemhf1o  13027  inffinp1  13043  isstructr  13090  setscomd  13116  imasbas  13383  imasplusg  13384  imasmulr  13385  subm0  13558  lssvancl1  14374  lssvnegcl  14383  lspprvacl  14420  lspsneli  14422  lspsn  14423  znf1o  14658  ntrin  14841  topssnei  14879  restbasg  14885  cnntri  14941  txcn  14992  txlm  14996  cnmpt2res  15014  psmetlecl  15051  xmetlecl  15084  bldisj  15118  bdmet  15219  bdbl  15220  bdmopn  15221  xmetxp  15224  metcnp  15229  tgioo  15271  cncfmet  15309  dedekindeulemlub  15337  suplociccreex  15341  ellimc3apf  15377  limcimolemlt  15381  limccnp2cntop  15394  dvfvalap  15398  dvidsslem  15410  dvmulxxbr  15419  dvaddxx  15420  dvmulxx  15421  dviaddf  15422  dvimulf  15423  dvcoapbr  15424  dvmptclx  15435  cxplt3  15637  cxpltd  15645  cxpled  15646  cxplt3d  15652  cxple3d  15653  logbrec  15677  logbgcd1irraplemap  15686  wilthlem1  15697  mpodvdsmulf1o  15707  lgslem1  15722  lgslem3  15724  lgsdirprm  15756  gausslemma2dlem1f1o  15782  gausslemma2dlem6  15789  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem4  15795  lgseisen  15796  lgsquadlem1  15799  lgsquad2lem1  15803  lgsquad3  15806  m1lgs  15807  2lgslem1a1  15808  2sqlem7  15843  usgredg2v  16068  vtxd0nedgbfi  16110  clwwlknonex2  16248  gsumgfsumlem  16633