Theorem syl22anc 1250

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 1247	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  5551  tfrexlem  6401  th3qlem1  6705  enpr2d  6885  ssenen  6921  phplem4dom  6932  phplem4on  6937  fiunsnnn  6951  findcard2sd  6962  unsnfi  6989  sbthlemi9  7040  endjusym  7171  endjudisj  7295  djuen  7296  ltanqg  7486  ltmnqg  7487  ltnnnq  7509  addcmpblnq0  7529  addlocprlemeqgt  7618  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  addcanprleml  7700  recexprlem1ssl  7719  caucvgprlemloc  7761  caucvgprprlemloccalc  7770  mulcmpblnr  7827  ltasrg  7856  recexgt0sr  7859  mulextsr1lem  7866  mulextsr1  7867  srpospr  7869  prsrlt  7873  ltpsrprg  7889  mappsrprg  7890  pitonnlem1p1  7932  recidpirq  7944  axpre-ltadd  7972  mulgt0d  8168  mul4d  8200  add4d  8214  add42d  8215  subcan  8300  addsub4d  8403  subadd4d  8404  sub4d  8405  2addsubd  8406  addsubeq4d  8407  muladdd  8461  mulsubd  8462  addgegt0d  8565  addgtge0d  8566  addge0d  8568  le2addd  8609  le2subd  8610  ltleaddd  8611  leltaddd  8612  lt2subd  8614  apreap  8633  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulap0r  8661  mulge0d  8667  mulap0d  8704  divdivdivap  8759  divcanap5  8760  divap0d  8852  recdivapd  8853  recdivap2d  8854  divcanap6d  8855  ddcanapd  8856  rec11apd  8857  divmuldivapd  8878  divmuleqapd  8879  subrecapd  8887  prodgt0  8898  lt2msq  8932  ledivdiv  8936  lediv12a  8940  recreclt  8946  divgt0d  8981  mulgt1d  8982  lemulge11d  8983  lemulge12d  8984  ltmul12ad  8987  lemul12ad  8988  lemul12bd  8989  nndivtr  9051  qreccl  9735  ledivdivd  9816  lediv12ad  9850  lt2mul2divd  9859  xlt2add  9974  xleaddadd  9981  iccss2  10038  iccssico2  10041  lincmb01cmp  10097  iccf1o  10098  fzrev2i  10180  qtri3or  10349  elicore  10375  2tnp1ge0ge0  10410  modqid  10460  q0mod  10466  q1mod  10467  modqabs  10468  modqadd1  10472  mulqaddmodid  10475  mulp1mod1  10476  modqmuladd  10477  modqmuladdnn0  10479  qnegmod  10480  m1modnnsub1  10481  addmodid  10483  modqm1p1mod0  10486  modqltm1p1mod  10487  modqmul1  10488  q2submod  10496  modifeq2int  10497  modaddmodup  10498  modaddmodlo  10499  modqaddmulmod  10502  modqsubdir  10504  modqeqmodmin  10505  modsumfzodifsn  10507  addmodlteq  10509  frecfzennn  10537  ser3mono  10598  expcl2lemap  10662  mulexpzap  10690  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  ltexp2a  10702  leexp2a  10703  sqdivap  10714  qsqeqor  10761  expnbnd  10774  expsubapd  10795  lt2sqd  10815  le2sqd  10816  sq11d  10817  apexp1  10829  bcp1nk  10873  hashunlem  10915  zfz1isolem1  10951  cjap  11090  cnreim  11162  resqrexlem1arp  11189  resqrexlemp1rp  11190  resqrexlemglsq  11206  abs00ap  11246  absext  11247  absexpzap  11264  absrele  11267  sqrtmuld  11353  sqrtsq2d  11354  sqrtled  11355  sqrtltd  11356  sqr11d  11357  abs3lemd  11385  minmax  11414  xrmaxiflemlub  11432  xrltmaxsup  11441  xrminmax  11449  xrbdtri  11460  climuni  11477  2clim  11485  addcn2  11494  mulcn2  11496  fsum3  11571  mptfzshft  11626  fsumrev  11627  fisum0diag2  11631  modfsummodlemstep  11641  binomlem  11667  mertenslemi1  11719  fprodrev  11803  efcllemp  11842  p1modz1  11978  dvds1  12037  dvdsext  12039  mulmoddvds  12047  oexpneg  12061  evennn02n  12066  evennn2n  12067  bitsinv1  12146  bezoutlemmo  12200  mulgcd  12210  dvdssqlem  12224  rpmulgcd2  12290  isprm6  12342  sqrt2irraplemnn  12374  sqrt2irrap  12375  crth  12419  eulerthlemh  12426  prmdiveq  12431  powm2modprm  12448  modprm0  12450  pythagtriplem2  12462  pythagtriplem11  12470  pythagtriplem13  12472  pythagtrip  12479  pcid  12520  pcgcd1  12524  pcprmpw2  12529  dvdsprmpweqle  12533  pcaddlem  12535  pcadd  12536  fldivp1  12544  4sqlem12  12598  4sqlem14  12600  4sqlem15  12601  4sqlem16  12602  unennn  12641  ennnfonelemg  12647  ennnfonelemhf1o  12657  inffinp1  12673  isstructr  12720  setscomd  12746  imasbas  13011  imasplusg  13012  imasmulr  13013  subm0  13186  lssvancl1  14001  lssvnegcl  14010  lspprvacl  14047  lspsneli  14049  lspsn  14050  znf1o  14285  ntrin  14468  topssnei  14506  restbasg  14512  cnntri  14568  txcn  14619  txlm  14623  cnmpt2res  14641  psmetlecl  14678  xmetlecl  14711  bldisj  14745  bdmet  14846  bdbl  14847  bdmopn  14848  xmetxp  14851  metcnp  14856  tgioo  14898  cncfmet  14936  dedekindeulemlub  14964  suplociccreex  14968  ellimc3apf  15004  limcimolemlt  15008  limccnp2cntop  15021  dvfvalap  15025  dvidsslem  15037  dvmulxxbr  15046  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvcoapbr  15051  dvmptclx  15062  cxplt3  15264  cxpltd  15272  cxpled  15273  cxplt3d  15279  cxple3d  15280  logbrec  15304  logbgcd1irraplemap  15313  wilthlem1  15324  mpodvdsmulf1o  15334  lgslem1  15349  lgslem3  15351  lgsdirprm  15383  gausslemma2dlem1f1o  15409  gausslemma2dlem6  15416  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem4  15422  lgseisen  15423  lgsquadlem1  15426  lgsquad2lem1  15430  lgsquad3  15433  m1lgs  15434  2lgslem1a1  15435  2sqlem7  15470