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  5545  tfrexlem  6389  th3qlem1  6693  enpr2d  6873  ssenen  6909  phplem4dom  6920  phplem4on  6925  fiunsnnn  6939  findcard2sd  6950  unsnfi  6977  sbthlemi9  7026  endjusym  7157  endjudisj  7272  djuen  7273  ltanqg  7462  ltmnqg  7463  ltnnnq  7485  addcmpblnq0  7505  addlocprlemeqgt  7594  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  addcanprleml  7676  recexprlem1ssl  7695  caucvgprlemloc  7737  caucvgprprlemloccalc  7746  mulcmpblnr  7803  ltasrg  7832  recexgt0sr  7835  mulextsr1lem  7842  mulextsr1  7843  srpospr  7845  prsrlt  7849  ltpsrprg  7865  mappsrprg  7866  pitonnlem1p1  7908  recidpirq  7920  axpre-ltadd  7948  mulgt0d  8144  mul4d  8176  add4d  8190  add42d  8191  subcan  8276  addsub4d  8379  subadd4d  8380  sub4d  8381  2addsubd  8382  addsubeq4d  8383  muladdd  8437  mulsubd  8438  addgegt0d  8540  addgtge0d  8541  addge0d  8543  le2addd  8584  le2subd  8585  ltleaddd  8586  leltaddd  8587  lt2subd  8589  apreap  8608  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  mulap0r  8636  mulge0d  8642  mulap0d  8679  divdivdivap  8734  divcanap5  8735  divap0d  8827  recdivapd  8828  recdivap2d  8829  divcanap6d  8830  ddcanapd  8831  rec11apd  8832  divmuldivapd  8853  divmuleqapd  8854  subrecapd  8862  prodgt0  8873  lt2msq  8907  ledivdiv  8911  lediv12a  8915  recreclt  8921  divgt0d  8956  mulgt1d  8957  lemulge11d  8958  lemulge12d  8959  ltmul12ad  8962  lemul12ad  8963  lemul12bd  8964  nndivtr  9026  qreccl  9710  ledivdivd  9791  lediv12ad  9825  lt2mul2divd  9834  xlt2add  9949  xleaddadd  9956  iccss2  10013  iccssico2  10016  lincmb01cmp  10072  iccf1o  10073  fzrev2i  10155  qtri3or  10313  elicore  10338  2tnp1ge0ge0  10373  modqid  10423  q0mod  10429  q1mod  10430  modqabs  10431  modqadd1  10435  mulqaddmodid  10438  mulp1mod1  10439  modqmuladd  10440  modqmuladdnn0  10442  qnegmod  10443  m1modnnsub1  10444  addmodid  10446  modqm1p1mod0  10449  modqltm1p1mod  10450  modqmul1  10451  q2submod  10459  modifeq2int  10460  modaddmodup  10461  modaddmodlo  10462  modqaddmulmod  10465  modqsubdir  10467  modqeqmodmin  10468  modsumfzodifsn  10470  addmodlteq  10472  frecfzennn  10500  ser3mono  10561  expcl2lemap  10625  mulexpzap  10653  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  ltexp2a  10665  leexp2a  10666  sqdivap  10677  qsqeqor  10724  expnbnd  10737  expsubapd  10758  lt2sqd  10778  le2sqd  10779  sq11d  10780  apexp1  10792  bcp1nk  10836  hashunlem  10878  zfz1isolem1  10914  cjap  11053  cnreim  11125  resqrexlem1arp  11152  resqrexlemp1rp  11153  resqrexlemglsq  11169  abs00ap  11209  absext  11210  absexpzap  11227  absrele  11230  sqrtmuld  11316  sqrtsq2d  11317  sqrtled  11318  sqrtltd  11319  sqr11d  11320  abs3lemd  11348  minmax  11376  xrmaxiflemlub  11394  xrltmaxsup  11403  xrminmax  11411  xrbdtri  11422  climuni  11439  2clim  11447  addcn2  11456  mulcn2  11458  fsum3  11533  mptfzshft  11588  fsumrev  11589  fisum0diag2  11593  modfsummodlemstep  11603  binomlem  11629  mertenslemi1  11681  fprodrev  11765  efcllemp  11804  p1modz1  11940  dvds1  11998  dvdsext  12000  mulmoddvds  12008  oexpneg  12021  evennn02n  12026  evennn2n  12027  bezoutlemmo  12146  mulgcd  12156  dvdssqlem  12170  rpmulgcd2  12236  isprm6  12288  sqrt2irraplemnn  12320  sqrt2irrap  12321  crth  12365  eulerthlemh  12372  prmdiveq  12377  powm2modprm  12393  modprm0  12395  pythagtriplem2  12407  pythagtriplem11  12415  pythagtriplem13  12417  pythagtrip  12424  pcid  12465  pcgcd1  12469  pcprmpw2  12474  dvdsprmpweqle  12478  pcaddlem  12480  pcadd  12481  fldivp1  12489  4sqlem12  12543  4sqlem14  12545  4sqlem15  12546  4sqlem16  12547  unennn  12557  ennnfonelemg  12563  ennnfonelemhf1o  12573  inffinp1  12589  isstructr  12636  setscomd  12662  imasbas  12893  imasplusg  12894  imasmulr  12895  subm0  13057  lssvancl1  13866  lssvnegcl  13875  lspprvacl  13912  lspsneli  13914  lspsn  13915  znf1o  14150  ntrin  14303  topssnei  14341  restbasg  14347  cnntri  14403  txcn  14454  txlm  14458  cnmpt2res  14476  psmetlecl  14513  xmetlecl  14546  bldisj  14580  bdmet  14681  bdbl  14682  bdmopn  14683  xmetxp  14686  metcnp  14691  tgioo  14733  cncfmet  14771  dedekindeulemlub  14799  suplociccreex  14803  ellimc3apf  14839  limcimolemlt  14843  limccnp2cntop  14856  dvfvalap  14860  dvidsslem  14872  dvmulxxbr  14881  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvcoapbr  14886  dvmptclx  14897  cxplt3  15095  cxpltd  15103  cxpled  15104  cxplt3d  15109  cxple3d  15110  logbrec  15133  logbgcd1irraplemap  15142  wilthlem1  15153  lgslem1  15157  lgslem3  15159  lgsdirprm  15191  gausslemma2dlem1f1o  15217  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquad2lem1  15238  lgsquad3  15241  m1lgs  15242  2lgslem1a1  15243  2sqlem7  15278