Theorem syl22anc 1279

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 1276	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  5683  tfrexlem  6599  th3qlem1  6905  en2prd  7100  enpr2d  7105  ssenen  7146  phplem4dom  7157  phplem4on  7163  fiunsnnn  7179  findcard2sd  7190  unsnfi  7220  sbthlemi9  7276  fsuppcorn  7295  endjusym  7430  endjudisj  7560  djuen  7561  ltanqg  7761  ltmnqg  7762  ltnnnq  7784  addcmpblnq0  7804  addlocprlemeqgt  7893  distrlem1prl  7943  distrlem1pru  7944  distrlem4prl  7945  distrlem4pru  7946  addcanprleml  7975  recexprlem1ssl  7994  caucvgprlemloc  8036  caucvgprprlemloccalc  8045  mulcmpblnr  8102  ltasrg  8131  recexgt0sr  8134  mulextsr1lem  8141  mulextsr1  8142  srpospr  8144  prsrlt  8148  ltpsrprg  8164  mappsrprg  8165  pitonnlem1p1  8207  recidpirq  8219  axpre-ltadd  8247  mulgt0d  8443  mul4d  8475  add4d  8489  add42d  8490  subcan  8575  addsub4d  8678  subadd4d  8679  sub4d  8680  2addsubd  8681  addsubeq4d  8682  muladdd  8737  mulsubd  8738  addgegt0d  8841  addgtge0d  8842  addge0d  8844  le2addd  8885  le2subd  8886  ltleaddd  8887  leltaddd  8888  lt2subd  8890  apreap  8909  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  mulap0r  8937  mulge0d  8943  mulap0d  8980  divdivdivap  9037  divcanap5  9038  divap0d  9130  recdivapd  9131  recdivap2d  9132  divcanap6d  9133  ddcanapd  9134  rec11apd  9135  divmuldivapd  9156  divmuleqapd  9157  subrecapd  9165  prodgt0  9176  lt2msq  9210  ledivdiv  9214  lediv12a  9218  recreclt  9224  divgt0d  9259  mulgt1d  9260  lemulge11d  9261  lemulge12d  9262  ltmul12ad  9265  lemul12ad  9266  lemul12bd  9267  nndivtr  9329  qreccl  10025  ledivdivd  10106  lediv12ad  10140  lt2mul2divd  10149  xlt2add  10265  xleaddadd  10272  iccss2  10329  iccssico2  10332  lincmb01cmp  10388  iccf1o  10390  fzrev2i  10476  qtri3or  10658  elicore  10684  2tnp1ge0ge0  10719  modqid  10769  q0mod  10775  q1mod  10776  modqabs  10777  modqadd1  10781  mulqaddmodid  10784  mulp1mod1  10785  modqmuladd  10786  modqmuladdnn0  10788  qnegmod  10789  m1modnnsub1  10790  addmodid  10792  modqm1p1mod0  10795  modqltm1p1mod  10796  modqmul1  10797  q2submod  10805  modifeq2int  10806  modaddmodup  10807  modaddmodlo  10808  modqaddmulmod  10811  modqsubdir  10813  modqeqmodmin  10814  modsumfzodifsn  10816  addmodlteq  10818  frecfzennn  10846  ser3mono  10907  expcl2lemap  10971  mulexpzap  10999  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  ltexp2a  11011  leexp2a  11012  sqdivap  11023  qsqeqor  11070  expnbnd  11084  expsubapd  11105  lt2sqd  11125  le2sqd  11126  sq11d  11127  apexp1  11139  bcp1nk  11183  hashunlem  11227  hashf1lem1  11268  zfz1isolem1  11275  hashtpgim  11280  sq01  11643  cjap  11655  cnreim  11727  resqrexlem1arp  11754  resqrexlemp1rp  11755  resqrexlemglsq  11771  abs00ap  11811  absext  11812  absexpzap  11829  absrele  11832  sqrtmuld  11918  sqrtsq2d  11919  sqrtled  11920  sqrtltd  11921  sqr11d  11922  abs3lemd  11950  minmax  11979  xrmaxiflemlub  11997  xrltmaxsup  12006  xrminmax  12014  xrbdtri  12025  climuni  12042  2clim  12050  addcn2  12059  mulcn2  12061  fsum3  12137  mptfzshft  12192  fsumrev  12193  fisum0diag2  12197  modfsummodlemstep  12207  binomlem  12233  mertenslemi1  12285  fprodrev  12369  efcllemp  12408  p1modz1  12544  dvds1  12603  dvdsext  12605  mulmoddvds  12613  oexpneg  12627  evennn02n  12632  evennn2n  12633  bitsinv1  12712  bezoutlemmo  12766  mulgcd  12776  dvdssqlem  12790  rpmulgcd2  12856  isprm6  12908  sqrt2irraplemnn  12940  sqrt2irrap  12941  crth  12985  eulerthlemh  12992  prmdiveq  12997  powm2modprm  13014  modprm0  13016  pythagtriplem2  13028  pythagtriplem11  13036  pythagtriplem13  13038  pythagtrip  13045  pcid  13086  pcgcd1  13090  pcprmpw2  13095  dvdsprmpweqle  13099  pcaddlem  13101  pcadd  13102  fldivp1  13110  4sqlem12  13164  4sqlem14  13166  4sqlem15  13167  4sqlem16  13168  ballotfilemsima  13242  ballotfilemfrceq  13255  unennn  13271  ennnfonelemg  13277  ennnfonelemhf1o  13287  inffinp1  13303  isstructr  13350  setscomd  13376  imasbas  13611  imasplusg  13612  imasmulr  13613  subm0  13772  gzsumshift  14132  gsump1  14140  lssvancl1  14687  lssvnegcl  14696  lspprvacl  14733  lspsneli  14735  lspsn  14736  znf1o  14969  ntrin  15208  topssnei  15246  restbasg  15252  cnntri  15308  txcn  15359  txlm  15363  cnmpt2res  15381  psmetlecl  15418  xmetlecl  15451  bldisj  15485  bdmet  15586  bdbl  15587  bdmopn  15588  xmetxp  15591  metcnp  15596  tgioo  15638  cncfmet  15676  dedekindeulemlub  15704  suplociccreex  15708  ellimc3apf  15744  limcimolemlt  15748  limccnp2cntop  15761  dvfvalap  15765  dvidsslem  15777  dvmulxxbr  15786  dvaddxx  15787  dvmulxx  15788  dviaddf  15789  dvimulf  15790  dvcoapbr  15791  dvmptclx  15802  cxplt3  16005  cxpltd  16013  cxpled  16014  cxplt3d  16020  cxple3d  16021  logbrec  16045  logbgcd1irraplemap  16054  log2tlbndlog2  16065  birthdaylem3  16072  pellexlem1  16074  pellexlem2  16075  wilthlem1  16077  mpodvdsmulf1o  16087  lgslem1  16102  lgslem3  16104  lgsdirprm  16136  gausslemma2dlem1f1o  16162  gausslemma2dlem6  16169  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem4  16175  lgseisen  16176  lgsquadlem1  16179  lgsquad2lem1  16183  lgsquad3  16186  m1lgs  16187  2lgslem1a1  16188  2sqlem7  16223  usgredg2v  16448  vtxd0nedgbfi  16523  clwwlknonex2  16663