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  5544  tfrexlem  6387  th3qlem1  6691  enpr2d  6871  ssenen  6907  phplem4dom  6918  phplem4on  6923  fiunsnnn  6937  findcard2sd  6948  unsnfi  6975  sbthlemi9  7024  endjusym  7155  endjudisj  7270  djuen  7271  ltanqg  7460  ltmnqg  7461  ltnnnq  7483  addcmpblnq0  7503  addlocprlemeqgt  7592  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  addcanprleml  7674  recexprlem1ssl  7693  caucvgprlemloc  7735  caucvgprprlemloccalc  7744  mulcmpblnr  7801  ltasrg  7830  recexgt0sr  7833  mulextsr1lem  7840  mulextsr1  7841  srpospr  7843  prsrlt  7847  ltpsrprg  7863  mappsrprg  7864  pitonnlem1p1  7906  recidpirq  7918  axpre-ltadd  7946  mulgt0d  8142  mul4d  8174  add4d  8188  add42d  8189  subcan  8274  addsub4d  8377  subadd4d  8378  sub4d  8379  2addsubd  8380  addsubeq4d  8381  muladdd  8435  mulsubd  8436  addgegt0d  8538  addgtge0d  8539  addge0d  8541  le2addd  8582  le2subd  8583  ltleaddd  8584  leltaddd  8585  lt2subd  8587  apreap  8606  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  mulap0r  8634  mulge0d  8640  mulap0d  8677  divdivdivap  8732  divcanap5  8733  divap0d  8825  recdivapd  8826  recdivap2d  8827  divcanap6d  8828  ddcanapd  8829  rec11apd  8830  divmuldivapd  8851  divmuleqapd  8852  subrecapd  8860  prodgt0  8871  lt2msq  8905  ledivdiv  8909  lediv12a  8913  recreclt  8919  divgt0d  8954  mulgt1d  8955  lemulge11d  8956  lemulge12d  8957  ltmul12ad  8960  lemul12ad  8961  lemul12bd  8962  nndivtr  9024  qreccl  9707  ledivdivd  9788  lediv12ad  9822  lt2mul2divd  9831  xlt2add  9946  xleaddadd  9953  iccss2  10010  iccssico2  10013  lincmb01cmp  10069  iccf1o  10070  fzrev2i  10152  qtri3or  10310  elicore  10335  2tnp1ge0ge0  10370  modqid  10420  q0mod  10426  q1mod  10427  modqabs  10428  modqadd1  10432  mulqaddmodid  10435  mulp1mod1  10436  modqmuladd  10437  modqmuladdnn0  10439  qnegmod  10440  m1modnnsub1  10441  addmodid  10443  modqm1p1mod0  10446  modqltm1p1mod  10447  modqmul1  10448  q2submod  10456  modifeq2int  10457  modaddmodup  10458  modaddmodlo  10459  modqaddmulmod  10462  modqsubdir  10464  modqeqmodmin  10465  modsumfzodifsn  10467  addmodlteq  10469  frecfzennn  10497  ser3mono  10558  expcl2lemap  10622  mulexpzap  10650  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  ltexp2a  10662  leexp2a  10663  sqdivap  10674  qsqeqor  10721  expnbnd  10734  expsubapd  10755  lt2sqd  10775  le2sqd  10776  sq11d  10777  apexp1  10789  bcp1nk  10833  hashunlem  10875  zfz1isolem1  10911  cjap  11050  cnreim  11122  resqrexlem1arp  11149  resqrexlemp1rp  11150  resqrexlemglsq  11166  abs00ap  11206  absext  11207  absexpzap  11224  absrele  11227  sqrtmuld  11313  sqrtsq2d  11314  sqrtled  11315  sqrtltd  11316  sqr11d  11317  abs3lemd  11345  minmax  11373  xrmaxiflemlub  11391  xrltmaxsup  11400  xrminmax  11408  xrbdtri  11419  climuni  11436  2clim  11444  addcn2  11453  mulcn2  11455  fsum3  11530  mptfzshft  11585  fsumrev  11586  fisum0diag2  11590  modfsummodlemstep  11600  binomlem  11626  mertenslemi1  11678  fprodrev  11762  efcllemp  11801  p1modz1  11937  dvds1  11995  dvdsext  11997  mulmoddvds  12005  oexpneg  12018  evennn02n  12023  evennn2n  12024  bezoutlemmo  12143  mulgcd  12153  dvdssqlem  12167  rpmulgcd2  12233  isprm6  12285  sqrt2irraplemnn  12317  sqrt2irrap  12318  crth  12362  eulerthlemh  12369  prmdiveq  12374  powm2modprm  12390  modprm0  12392  pythagtriplem2  12404  pythagtriplem11  12412  pythagtriplem13  12414  pythagtrip  12421  pcid  12462  pcgcd1  12466  pcprmpw2  12471  dvdsprmpweqle  12475  pcaddlem  12477  pcadd  12478  fldivp1  12486  4sqlem12  12540  4sqlem14  12542  4sqlem15  12543  4sqlem16  12544  unennn  12554  ennnfonelemg  12560  ennnfonelemhf1o  12570  inffinp1  12586  isstructr  12633  setscomd  12659  imasbas  12890  imasplusg  12891  imasmulr  12892  subm0  13054  lssvancl1  13863  lssvnegcl  13872  lspprvacl  13909  lspsneli  13911  lspsn  13912  znf1o  14139  ntrin  14292  topssnei  14330  restbasg  14336  cnntri  14392  txcn  14443  txlm  14447  cnmpt2res  14465  psmetlecl  14502  xmetlecl  14535  bldisj  14569  bdmet  14670  bdbl  14671  bdmopn  14672  xmetxp  14675  metcnp  14680  tgioo  14714  cncfmet  14747  dedekindeulemlub  14774  suplociccreex  14778  ellimc3apf  14814  limcimolemlt  14818  limccnp2cntop  14831  dvfvalap  14835  dvmulxxbr  14851  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvcoapbr  14856  dvmptclx  14865  cxplt3  15054  cxpltd  15062  cxpled  15063  cxplt3d  15068  cxple3d  15069  logbrec  15092  logbgcd1irraplemap  15101  wilthlem1  15112  lgslem1  15116  lgslem3  15118  lgsdirprm  15150  gausslemma2dlem1f1o  15176  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2sqlem7  15208