Theorem syl22anc 1253

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 1250	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  5593  tfrexlem  6450  th3qlem1  6754  en2prd  6940  enpr2d  6942  ssenen  6980  phplem4dom  6991  phplem4on  6997  fiunsnnn  7011  findcard2sd  7022  unsnfi  7049  sbthlemi9  7100  endjusym  7231  endjudisj  7360  djuen  7361  ltanqg  7555  ltmnqg  7556  ltnnnq  7578  addcmpblnq0  7598  addlocprlemeqgt  7687  distrlem1prl  7737  distrlem1pru  7738  distrlem4prl  7739  distrlem4pru  7740  addcanprleml  7769  recexprlem1ssl  7788  caucvgprlemloc  7830  caucvgprprlemloccalc  7839  mulcmpblnr  7896  ltasrg  7925  recexgt0sr  7928  mulextsr1lem  7935  mulextsr1  7936  srpospr  7938  prsrlt  7942  ltpsrprg  7958  mappsrprg  7959  pitonnlem1p1  8001  recidpirq  8013  axpre-ltadd  8041  mulgt0d  8237  mul4d  8269  add4d  8283  add42d  8284  subcan  8369  addsub4d  8472  subadd4d  8473  sub4d  8474  2addsubd  8475  addsubeq4d  8476  muladdd  8530  mulsubd  8531  addgegt0d  8634  addgtge0d  8635  addge0d  8637  le2addd  8678  le2subd  8679  ltleaddd  8680  leltaddd  8681  lt2subd  8683  apreap  8702  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  mulap0r  8730  mulge0d  8736  mulap0d  8773  divdivdivap  8828  divcanap5  8829  divap0d  8921  recdivapd  8922  recdivap2d  8923  divcanap6d  8924  ddcanapd  8925  rec11apd  8926  divmuldivapd  8947  divmuleqapd  8948  subrecapd  8956  prodgt0  8967  lt2msq  9001  ledivdiv  9005  lediv12a  9009  recreclt  9015  divgt0d  9050  mulgt1d  9051  lemulge11d  9052  lemulge12d  9053  ltmul12ad  9056  lemul12ad  9057  lemul12bd  9058  nndivtr  9120  qreccl  9805  ledivdivd  9886  lediv12ad  9920  lt2mul2divd  9929  xlt2add  10044  xleaddadd  10051  iccss2  10108  iccssico2  10111  lincmb01cmp  10167  iccf1o  10168  fzrev2i  10250  qtri3or  10427  elicore  10453  2tnp1ge0ge0  10488  modqid  10538  q0mod  10544  q1mod  10545  modqabs  10546  modqadd1  10550  mulqaddmodid  10553  mulp1mod1  10554  modqmuladd  10555  modqmuladdnn0  10557  qnegmod  10558  m1modnnsub1  10559  addmodid  10561  modqm1p1mod0  10564  modqltm1p1mod  10565  modqmul1  10566  q2submod  10574  modifeq2int  10575  modaddmodup  10576  modaddmodlo  10577  modqaddmulmod  10580  modqsubdir  10582  modqeqmodmin  10583  modsumfzodifsn  10585  addmodlteq  10587  frecfzennn  10615  ser3mono  10676  expcl2lemap  10740  mulexpzap  10768  expaddzaplem  10771  expaddzap  10772  expmulzap  10774  ltexp2a  10780  leexp2a  10781  sqdivap  10792  qsqeqor  10839  expnbnd  10852  expsubapd  10873  lt2sqd  10893  le2sqd  10894  sq11d  10895  apexp1  10907  bcp1nk  10951  hashunlem  10993  zfz1isolem1  11029  cjap  11383  cnreim  11455  resqrexlem1arp  11482  resqrexlemp1rp  11483  resqrexlemglsq  11499  abs00ap  11539  absext  11540  absexpzap  11557  absrele  11560  sqrtmuld  11646  sqrtsq2d  11647  sqrtled  11648  sqrtltd  11649  sqr11d  11650  abs3lemd  11678  minmax  11707  xrmaxiflemlub  11725  xrltmaxsup  11734  xrminmax  11742  xrbdtri  11753  climuni  11770  2clim  11778  addcn2  11787  mulcn2  11789  fsum3  11864  mptfzshft  11919  fsumrev  11920  fisum0diag2  11924  modfsummodlemstep  11934  binomlem  11960  mertenslemi1  12012  fprodrev  12096  efcllemp  12135  p1modz1  12271  dvds1  12330  dvdsext  12332  mulmoddvds  12340  oexpneg  12354  evennn02n  12359  evennn2n  12360  bitsinv1  12439  bezoutlemmo  12493  mulgcd  12503  dvdssqlem  12517  rpmulgcd2  12583  isprm6  12635  sqrt2irraplemnn  12667  sqrt2irrap  12668  crth  12712  eulerthlemh  12719  prmdiveq  12724  powm2modprm  12741  modprm0  12743  pythagtriplem2  12755  pythagtriplem11  12763  pythagtriplem13  12765  pythagtrip  12772  pcid  12813  pcgcd1  12817  pcprmpw2  12822  dvdsprmpweqle  12826  pcaddlem  12828  pcadd  12829  fldivp1  12837  4sqlem12  12891  4sqlem14  12893  4sqlem15  12894  4sqlem16  12895  unennn  12934  ennnfonelemg  12940  ennnfonelemhf1o  12950  inffinp1  12966  isstructr  13013  setscomd  13039  imasbas  13306  imasplusg  13307  imasmulr  13308  subm0  13481  lssvancl1  14296  lssvnegcl  14305  lspprvacl  14342  lspsneli  14344  lspsn  14345  znf1o  14580  ntrin  14763  topssnei  14801  restbasg  14807  cnntri  14863  txcn  14914  txlm  14918  cnmpt2res  14936  psmetlecl  14973  xmetlecl  15006  bldisj  15040  bdmet  15141  bdbl  15142  bdmopn  15143  xmetxp  15146  metcnp  15151  tgioo  15193  cncfmet  15231  dedekindeulemlub  15259  suplociccreex  15263  ellimc3apf  15299  limcimolemlt  15303  limccnp2cntop  15316  dvfvalap  15320  dvidsslem  15332  dvmulxxbr  15341  dvaddxx  15342  dvmulxx  15343  dviaddf  15344  dvimulf  15345  dvcoapbr  15346  dvmptclx  15357  cxplt3  15559  cxpltd  15567  cxpled  15568  cxplt3d  15574  cxple3d  15575  logbrec  15599  logbgcd1irraplemap  15608  wilthlem1  15619  mpodvdsmulf1o  15629  lgslem1  15644  lgslem3  15646  lgsdirprm  15678  gausslemma2dlem1f1o  15704  gausslemma2dlem6  15711  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem4  15717  lgseisen  15718  lgsquadlem1  15721  lgsquad2lem1  15725  lgsquad3  15728  m1lgs  15729  2lgslem1a1  15730  2sqlem7  15765  usgredg2v  15987