Theorem syl22anc 1239

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 1236	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  5507  tfrexlem  6337  th3qlem1  6639  enpr2d  6819  ssenen  6853  phplem4dom  6864  phplem4on  6869  fiunsnnn  6883  findcard2sd  6894  unsnfi  6920  sbthlemi9  6966  endjusym  7097  endjudisj  7211  djuen  7212  ltanqg  7401  ltmnqg  7402  ltnnnq  7424  addcmpblnq0  7444  addlocprlemeqgt  7533  distrlem1prl  7583  distrlem1pru  7584  distrlem4prl  7585  distrlem4pru  7586  addcanprleml  7615  recexprlem1ssl  7634  caucvgprlemloc  7676  caucvgprprlemloccalc  7685  mulcmpblnr  7742  ltasrg  7771  recexgt0sr  7774  mulextsr1lem  7781  mulextsr1  7782  srpospr  7784  prsrlt  7788  ltpsrprg  7804  mappsrprg  7805  pitonnlem1p1  7847  recidpirq  7859  axpre-ltadd  7887  mulgt0d  8082  mul4d  8114  add4d  8128  add42d  8129  subcan  8214  addsub4d  8317  subadd4d  8318  sub4d  8319  2addsubd  8320  addsubeq4d  8321  muladdd  8375  mulsubd  8376  addgegt0d  8478  addgtge0d  8479  addge0d  8481  le2addd  8522  le2subd  8523  ltleaddd  8524  leltaddd  8525  lt2subd  8527  apreap  8546  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  mulap0r  8574  mulge0d  8580  mulap0d  8617  divdivdivap  8672  divcanap5  8673  divap0d  8765  recdivapd  8766  recdivap2d  8767  divcanap6d  8768  ddcanapd  8769  rec11apd  8770  divmuldivapd  8791  divmuleqapd  8792  subrecapd  8800  prodgt0  8811  lt2msq  8845  ledivdiv  8849  lediv12a  8853  recreclt  8859  divgt0d  8894  mulgt1d  8895  lemulge11d  8896  lemulge12d  8897  ltmul12ad  8900  lemul12ad  8901  lemul12bd  8902  nndivtr  8963  qreccl  9644  ledivdivd  9724  lediv12ad  9758  lt2mul2divd  9767  xlt2add  9882  xleaddadd  9889  iccss2  9946  iccssico2  9949  lincmb01cmp  10005  iccf1o  10006  fzrev2i  10088  qtri3or  10245  elicore  10269  2tnp1ge0ge0  10303  modqid  10351  q0mod  10357  q1mod  10358  modqabs  10359  modqadd1  10363  mulqaddmodid  10366  mulp1mod1  10367  modqmuladd  10368  modqmuladdnn0  10370  qnegmod  10371  m1modnnsub1  10372  addmodid  10374  modqm1p1mod0  10377  modqltm1p1mod  10378  modqmul1  10379  q2submod  10387  modifeq2int  10388  modaddmodup  10389  modaddmodlo  10390  modqaddmulmod  10393  modqsubdir  10395  modqeqmodmin  10396  modsumfzodifsn  10398  addmodlteq  10400  frecfzennn  10428  ser3mono  10480  expcl2lemap  10534  mulexpzap  10562  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  ltexp2a  10574  leexp2a  10575  sqdivap  10586  qsqeqor  10633  expnbnd  10646  expsubapd  10667  lt2sqd  10687  le2sqd  10688  sq11d  10689  apexp1  10700  bcp1nk  10744  hashunlem  10786  zfz1isolem1  10822  cjap  10917  cnreim  10989  resqrexlem1arp  11016  resqrexlemp1rp  11017  resqrexlemglsq  11033  abs00ap  11073  absext  11074  absexpzap  11091  absrele  11094  sqrtmuld  11180  sqrtsq2d  11181  sqrtled  11182  sqrtltd  11183  sqr11d  11184  abs3lemd  11212  minmax  11240  xrmaxiflemlub  11258  xrltmaxsup  11267  xrminmax  11275  xrbdtri  11286  climuni  11303  2clim  11311  addcn2  11320  mulcn2  11322  fsum3  11397  mptfzshft  11452  fsumrev  11453  fisum0diag2  11457  modfsummodlemstep  11467  binomlem  11493  mertenslemi1  11545  fprodrev  11629  efcllemp  11668  p1modz1  11803  dvds1  11861  dvdsext  11863  mulmoddvds  11871  oexpneg  11884  evennn02n  11889  evennn2n  11890  bezoutlemmo  12009  mulgcd  12019  dvdssqlem  12033  rpmulgcd2  12097  isprm6  12149  sqrt2irraplemnn  12181  sqrt2irrap  12182  crth  12226  eulerthlemh  12233  prmdiveq  12238  powm2modprm  12254  modprm0  12256  pythagtriplem2  12268  pythagtriplem11  12276  pythagtriplem13  12278  pythagtrip  12285  pcid  12325  pcgcd1  12329  pcprmpw2  12334  dvdsprmpweqle  12338  pcaddlem  12340  pcadd  12341  fldivp1  12348  unennn  12400  ennnfonelemg  12406  ennnfonelemhf1o  12416  inffinp1  12432  isstructr  12479  setscomd  12505  imasbas  12733  imasplusg  12734  imasmulr  12735  lssvancl1  13458  lssvnegcl  13468  lspprvacl  13504  lspsneli  13506  lspsn  13507  ntrin  13709  topssnei  13747  restbasg  13753  cnntri  13809  txcn  13860  txlm  13864  cnmpt2res  13882  psmetlecl  13919  xmetlecl  13952  bldisj  13986  bdmet  14087  bdbl  14088  bdmopn  14089  xmetxp  14092  metcnp  14097  tgioo  14131  cncfmet  14164  dedekindeulemlub  14183  suplociccreex  14187  ellimc3apf  14214  limcimolemlt  14218  limccnp2cntop  14231  dvfvalap  14235  dvmulxxbr  14251  dvaddxx  14252  dvmulxx  14253  dviaddf  14254  dvimulf  14255  dvcoapbr  14256  dvmptclx  14265  cxplt3  14425  cxpltd  14433  cxpled  14434  cxplt3d  14439  cxple3d  14440  logbrec  14463  logbgcd1irraplemap  14472  lgslem1  14486  lgslem3  14488  lgsdirprm  14520  lgseisenlem1  14535  lgseisenlem2  14536  m1lgs  14537  2sqlem7  14553