Theorem syl22anc 1275

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 1272	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  5659  tfrexlem  6564  th3qlem1  6870  en2prd  7058  enpr2d  7063  ssenen  7104  phplem4dom  7115  phplem4on  7121  fiunsnnn  7137  findcard2sd  7148  unsnfi  7178  sbthlemi9  7234  fsuppcorn  7253  endjusym  7386  endjudisj  7516  djuen  7517  ltanqg  7711  ltmnqg  7712  ltnnnq  7734  addcmpblnq0  7754  addlocprlemeqgt  7843  distrlem1prl  7893  distrlem1pru  7894  distrlem4prl  7895  distrlem4pru  7896  addcanprleml  7925  recexprlem1ssl  7944  caucvgprlemloc  7986  caucvgprprlemloccalc  7995  mulcmpblnr  8052  ltasrg  8081  recexgt0sr  8084  mulextsr1lem  8091  mulextsr1  8092  srpospr  8094  prsrlt  8098  ltpsrprg  8114  mappsrprg  8115  pitonnlem1p1  8157  recidpirq  8169  axpre-ltadd  8197  mulgt0d  8392  mul4d  8424  add4d  8438  add42d  8439  subcan  8524  addsub4d  8627  subadd4d  8628  sub4d  8629  2addsubd  8630  addsubeq4d  8631  muladdd  8685  mulsubd  8686  addgegt0d  8789  addgtge0d  8790  addge0d  8792  le2addd  8833  le2subd  8834  ltleaddd  8835  leltaddd  8836  lt2subd  8838  apreap  8857  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  mulap0r  8885  mulge0d  8891  mulap0d  8928  divdivdivap  8983  divcanap5  8984  divap0d  9076  recdivapd  9077  recdivap2d  9078  divcanap6d  9079  ddcanapd  9080  rec11apd  9081  divmuldivapd  9102  divmuleqapd  9103  subrecapd  9111  prodgt0  9122  lt2msq  9156  ledivdiv  9160  lediv12a  9164  recreclt  9170  divgt0d  9205  mulgt1d  9206  lemulge11d  9207  lemulge12d  9208  ltmul12ad  9211  lemul12ad  9212  lemul12bd  9213  nndivtr  9275  qreccl  9970  ledivdivd  10051  lediv12ad  10085  lt2mul2divd  10094  xlt2add  10209  xleaddadd  10216  iccss2  10273  iccssico2  10276  lincmb01cmp  10332  iccf1o  10334  fzrev2i  10416  qtri3or  10596  elicore  10622  2tnp1ge0ge0  10657  modqid  10707  q0mod  10713  q1mod  10714  modqabs  10715  modqadd1  10719  mulqaddmodid  10722  mulp1mod1  10723  modqmuladd  10724  modqmuladdnn0  10726  qnegmod  10727  m1modnnsub1  10728  addmodid  10730  modqm1p1mod0  10733  modqltm1p1mod  10734  modqmul1  10735  q2submod  10743  modifeq2int  10744  modaddmodup  10745  modaddmodlo  10746  modqaddmulmod  10749  modqsubdir  10751  modqeqmodmin  10752  modsumfzodifsn  10754  addmodlteq  10756  frecfzennn  10784  ser3mono  10845  expcl2lemap  10909  mulexpzap  10937  expaddzaplem  10940  expaddzap  10941  expmulzap  10943  ltexp2a  10949  leexp2a  10950  sqdivap  10961  qsqeqor  11008  expnbnd  11021  expsubapd  11042  lt2sqd  11062  le2sqd  11063  sq11d  11064  apexp1  11076  bcp1nk  11120  hashunlem  11163  zfz1isolem1  11205  hashtpgim  11210  cjap  11584  cnreim  11656  resqrexlem1arp  11683  resqrexlemp1rp  11684  resqrexlemglsq  11700  abs00ap  11740  absext  11741  absexpzap  11758  absrele  11761  sqrtmuld  11847  sqrtsq2d  11848  sqrtled  11849  sqrtltd  11850  sqr11d  11851  abs3lemd  11879  minmax  11908  xrmaxiflemlub  11926  xrltmaxsup  11935  xrminmax  11943  xrbdtri  11954  climuni  11971  2clim  11979  addcn2  11988  mulcn2  11990  fsum3  12066  mptfzshft  12121  fsumrev  12122  fisum0diag2  12126  modfsummodlemstep  12136  binomlem  12162  mertenslemi1  12214  fprodrev  12298  efcllemp  12337  p1modz1  12473  dvds1  12532  dvdsext  12534  mulmoddvds  12542  oexpneg  12556  evennn02n  12561  evennn2n  12562  bitsinv1  12641  bezoutlemmo  12695  mulgcd  12705  dvdssqlem  12719  rpmulgcd2  12785  isprm6  12837  sqrt2irraplemnn  12869  sqrt2irrap  12870  crth  12914  eulerthlemh  12921  prmdiveq  12926  powm2modprm  12943  modprm0  12945  pythagtriplem2  12957  pythagtriplem11  12965  pythagtriplem13  12967  pythagtrip  12974  pcid  13015  pcgcd1  13019  pcprmpw2  13024  dvdsprmpweqle  13028  pcaddlem  13030  pcadd  13031  fldivp1  13039  4sqlem12  13093  4sqlem14  13095  4sqlem15  13096  4sqlem16  13097  unennn  13137  ennnfonelemg  13143  ennnfonelemhf1o  13153  inffinp1  13169  isstructr  13216  setscomd  13242  imasbas  13509  imasplusg  13510  imasmulr  13511  subm0  13684  lssvancl1  14502  lssvnegcl  14511  lspprvacl  14548  lspsneli  14550  lspsn  14551  znf1o  14786  ntrin  14976  topssnei  15014  restbasg  15020  cnntri  15076  txcn  15127  txlm  15131  cnmpt2res  15149  psmetlecl  15186  xmetlecl  15219  bldisj  15253  bdmet  15354  bdbl  15355  bdmopn  15356  xmetxp  15359  metcnp  15364  tgioo  15406  cncfmet  15444  dedekindeulemlub  15472  suplociccreex  15476  ellimc3apf  15512  limcimolemlt  15516  limccnp2cntop  15529  dvfvalap  15533  dvidsslem  15545  dvmulxxbr  15554  dvaddxx  15555  dvmulxx  15556  dviaddf  15557  dvimulf  15558  dvcoapbr  15559  dvmptclx  15570  cxplt3  15772  cxpltd  15780  cxpled  15781  cxplt3d  15787  cxple3d  15788  logbrec  15812  logbgcd1irraplemap  15821  pellexlem1  15832  pellexlem2  15833  wilthlem1  15835  mpodvdsmulf1o  15845  lgslem1  15860  lgslem3  15862  lgsdirprm  15894  gausslemma2dlem1f1o  15920  gausslemma2dlem6  15927  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem4  15933  lgseisen  15934  lgsquadlem1  15937  lgsquad2lem1  15941  lgsquad3  15944  m1lgs  15945  2lgslem1a1  15946  2sqlem7  15981  usgredg2v  16206  vtxd0nedgbfi  16281  clwwlknonex2  16421  gsumgfsumlem  16851  gfsump1  16854