Theorem syl22anc 1249

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 1246	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  5519  tfrexlem  6352  th3qlem1  6654  enpr2d  6834  ssenen  6868  phplem4dom  6879  phplem4on  6884  fiunsnnn  6898  findcard2sd  6909  unsnfi  6935  sbthlemi9  6981  endjusym  7112  endjudisj  7226  djuen  7227  ltanqg  7416  ltmnqg  7417  ltnnnq  7439  addcmpblnq0  7459  addlocprlemeqgt  7548  distrlem1prl  7598  distrlem1pru  7599  distrlem4prl  7600  distrlem4pru  7601  addcanprleml  7630  recexprlem1ssl  7649  caucvgprlemloc  7691  caucvgprprlemloccalc  7700  mulcmpblnr  7757  ltasrg  7786  recexgt0sr  7789  mulextsr1lem  7796  mulextsr1  7797  srpospr  7799  prsrlt  7803  ltpsrprg  7819  mappsrprg  7820  pitonnlem1p1  7862  recidpirq  7874  axpre-ltadd  7902  mulgt0d  8097  mul4d  8129  add4d  8143  add42d  8144  subcan  8229  addsub4d  8332  subadd4d  8333  sub4d  8334  2addsubd  8335  addsubeq4d  8336  muladdd  8390  mulsubd  8391  addgegt0d  8493  addgtge0d  8494  addge0d  8496  le2addd  8537  le2subd  8538  ltleaddd  8539  leltaddd  8540  lt2subd  8542  apreap  8561  apsym  8580  apcotr  8581  apadd1  8582  apneg  8585  mulext1  8586  mulap0r  8589  mulge0d  8595  mulap0d  8632  divdivdivap  8687  divcanap5  8688  divap0d  8780  recdivapd  8781  recdivap2d  8782  divcanap6d  8783  ddcanapd  8784  rec11apd  8785  divmuldivapd  8806  divmuleqapd  8807  subrecapd  8815  prodgt0  8826  lt2msq  8860  ledivdiv  8864  lediv12a  8868  recreclt  8874  divgt0d  8909  mulgt1d  8910  lemulge11d  8911  lemulge12d  8912  ltmul12ad  8915  lemul12ad  8916  lemul12bd  8917  nndivtr  8978  qreccl  9659  ledivdivd  9739  lediv12ad  9773  lt2mul2divd  9782  xlt2add  9897  xleaddadd  9904  iccss2  9961  iccssico2  9964  lincmb01cmp  10020  iccf1o  10021  fzrev2i  10103  qtri3or  10260  elicore  10284  2tnp1ge0ge0  10318  modqid  10366  q0mod  10372  q1mod  10373  modqabs  10374  modqadd1  10378  mulqaddmodid  10381  mulp1mod1  10382  modqmuladd  10383  modqmuladdnn0  10385  qnegmod  10386  m1modnnsub1  10387  addmodid  10389  modqm1p1mod0  10392  modqltm1p1mod  10393  modqmul1  10394  q2submod  10402  modifeq2int  10403  modaddmodup  10404  modaddmodlo  10405  modqaddmulmod  10408  modqsubdir  10410  modqeqmodmin  10411  modsumfzodifsn  10413  addmodlteq  10415  frecfzennn  10443  ser3mono  10495  expcl2lemap  10549  mulexpzap  10577  expaddzaplem  10580  expaddzap  10581  expmulzap  10583  ltexp2a  10589  leexp2a  10590  sqdivap  10601  qsqeqor  10648  expnbnd  10661  expsubapd  10682  lt2sqd  10702  le2sqd  10703  sq11d  10704  apexp1  10715  bcp1nk  10759  hashunlem  10801  zfz1isolem1  10837  cjap  10932  cnreim  11004  resqrexlem1arp  11031  resqrexlemp1rp  11032  resqrexlemglsq  11048  abs00ap  11088  absext  11089  absexpzap  11106  absrele  11109  sqrtmuld  11195  sqrtsq2d  11196  sqrtled  11197  sqrtltd  11198  sqr11d  11199  abs3lemd  11227  minmax  11255  xrmaxiflemlub  11273  xrltmaxsup  11282  xrminmax  11290  xrbdtri  11301  climuni  11318  2clim  11326  addcn2  11335  mulcn2  11337  fsum3  11412  mptfzshft  11467  fsumrev  11468  fisum0diag2  11472  modfsummodlemstep  11482  binomlem  11508  mertenslemi1  11560  fprodrev  11644  efcllemp  11683  p1modz1  11818  dvds1  11876  dvdsext  11878  mulmoddvds  11886  oexpneg  11899  evennn02n  11904  evennn2n  11905  bezoutlemmo  12024  mulgcd  12034  dvdssqlem  12048  rpmulgcd2  12112  isprm6  12164  sqrt2irraplemnn  12196  sqrt2irrap  12197  crth  12241  eulerthlemh  12248  prmdiveq  12253  powm2modprm  12269  modprm0  12271  pythagtriplem2  12283  pythagtriplem11  12291  pythagtriplem13  12293  pythagtrip  12300  pcid  12340  pcgcd1  12344  pcprmpw2  12349  dvdsprmpweqle  12353  pcaddlem  12355  pcadd  12356  fldivp1  12363  unennn  12415  ennnfonelemg  12421  ennnfonelemhf1o  12431  inffinp1  12447  isstructr  12494  setscomd  12520  imasbas  12749  imasplusg  12750  imasmulr  12751  subm0  12899  lssvancl1  13643  lssvnegcl  13652  lspprvacl  13689  lspsneli  13691  lspsn  13692  ntrin  14007  topssnei  14045  restbasg  14051  cnntri  14107  txcn  14158  txlm  14162  cnmpt2res  14180  psmetlecl  14217  xmetlecl  14250  bldisj  14284  bdmet  14385  bdbl  14386  bdmopn  14387  xmetxp  14390  metcnp  14395  tgioo  14429  cncfmet  14462  dedekindeulemlub  14481  suplociccreex  14485  ellimc3apf  14512  limcimolemlt  14516  limccnp2cntop  14529  dvfvalap  14533  dvmulxxbr  14549  dvaddxx  14550  dvmulxx  14551  dviaddf  14552  dvimulf  14553  dvcoapbr  14554  dvmptclx  14563  cxplt3  14723  cxpltd  14731  cxpled  14732  cxplt3d  14737  cxple3d  14738  logbrec  14761  logbgcd1irraplemap  14770  lgslem1  14784  lgslem3  14786  lgsdirprm  14818  lgseisenlem1  14833  lgseisenlem2  14834  m1lgs  14835  2sqlem7  14851