Theorem syl22anc 1274

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 1271	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  5629  tfrexlem  6500  th3qlem1  6806  en2prd  6992  enpr2d  6997  ssenen  7037  phplem4dom  7048  phplem4on  7054  fiunsnnn  7070  findcard2sd  7081  unsnfi  7111  sbthlemi9  7164  endjusym  7295  endjudisj  7425  djuen  7426  ltanqg  7620  ltmnqg  7621  ltnnnq  7643  addcmpblnq0  7663  addlocprlemeqgt  7752  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  addcanprleml  7834  recexprlem1ssl  7853  caucvgprlemloc  7895  caucvgprprlemloccalc  7904  mulcmpblnr  7961  ltasrg  7990  recexgt0sr  7993  mulextsr1lem  8000  mulextsr1  8001  srpospr  8003  prsrlt  8007  ltpsrprg  8023  mappsrprg  8024  pitonnlem1p1  8066  recidpirq  8078  axpre-ltadd  8106  mulgt0d  8302  mul4d  8334  add4d  8348  add42d  8349  subcan  8434  addsub4d  8537  subadd4d  8538  sub4d  8539  2addsubd  8540  addsubeq4d  8541  muladdd  8595  mulsubd  8596  addgegt0d  8699  addgtge0d  8700  addge0d  8702  le2addd  8743  le2subd  8744  ltleaddd  8745  leltaddd  8746  lt2subd  8748  apreap  8767  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulap0r  8795  mulge0d  8801  mulap0d  8838  divdivdivap  8893  divcanap5  8894  divap0d  8986  recdivapd  8987  recdivap2d  8988  divcanap6d  8989  ddcanapd  8990  rec11apd  8991  divmuldivapd  9012  divmuleqapd  9013  subrecapd  9021  prodgt0  9032  lt2msq  9066  ledivdiv  9070  lediv12a  9074  recreclt  9080  divgt0d  9115  mulgt1d  9116  lemulge11d  9117  lemulge12d  9118  ltmul12ad  9121  lemul12ad  9122  lemul12bd  9123  nndivtr  9185  qreccl  9876  ledivdivd  9957  lediv12ad  9991  lt2mul2divd  10000  xlt2add  10115  xleaddadd  10122  iccss2  10179  iccssico2  10182  lincmb01cmp  10238  iccf1o  10239  fzrev2i  10321  qtri3or  10501  elicore  10527  2tnp1ge0ge0  10562  modqid  10612  q0mod  10618  q1mod  10619  modqabs  10620  modqadd1  10624  mulqaddmodid  10627  mulp1mod1  10628  modqmuladd  10629  modqmuladdnn0  10631  qnegmod  10632  m1modnnsub1  10633  addmodid  10635  modqm1p1mod0  10638  modqltm1p1mod  10639  modqmul1  10640  q2submod  10648  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modqaddmulmod  10654  modqsubdir  10656  modqeqmodmin  10657  modsumfzodifsn  10659  addmodlteq  10661  frecfzennn  10689  ser3mono  10750  expcl2lemap  10814  mulexpzap  10842  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  ltexp2a  10854  leexp2a  10855  sqdivap  10866  qsqeqor  10913  expnbnd  10926  expsubapd  10947  lt2sqd  10967  le2sqd  10968  sq11d  10969  apexp1  10981  bcp1nk  11025  hashunlem  11068  zfz1isolem1  11105  cjap  11468  cnreim  11540  resqrexlem1arp  11567  resqrexlemp1rp  11568  resqrexlemglsq  11584  abs00ap  11624  absext  11625  absexpzap  11642  absrele  11645  sqrtmuld  11731  sqrtsq2d  11732  sqrtled  11733  sqrtltd  11734  sqr11d  11735  abs3lemd  11763  minmax  11792  xrmaxiflemlub  11810  xrltmaxsup  11819  xrminmax  11827  xrbdtri  11838  climuni  11855  2clim  11863  addcn2  11872  mulcn2  11874  fsum3  11950  mptfzshft  12005  fsumrev  12006  fisum0diag2  12010  modfsummodlemstep  12020  binomlem  12046  mertenslemi1  12098  fprodrev  12182  efcllemp  12221  p1modz1  12357  dvds1  12416  dvdsext  12418  mulmoddvds  12426  oexpneg  12440  evennn02n  12445  evennn2n  12446  bitsinv1  12525  bezoutlemmo  12579  mulgcd  12589  dvdssqlem  12603  rpmulgcd2  12669  isprm6  12721  sqrt2irraplemnn  12753  sqrt2irrap  12754  crth  12798  eulerthlemh  12805  prmdiveq  12810  powm2modprm  12827  modprm0  12829  pythagtriplem2  12841  pythagtriplem11  12849  pythagtriplem13  12851  pythagtrip  12858  pcid  12899  pcgcd1  12903  pcprmpw2  12908  dvdsprmpweqle  12912  pcaddlem  12914  pcadd  12915  fldivp1  12923  4sqlem12  12977  4sqlem14  12979  4sqlem15  12980  4sqlem16  12981  unennn  13020  ennnfonelemg  13026  ennnfonelemhf1o  13036  inffinp1  13052  isstructr  13099  setscomd  13125  imasbas  13392  imasplusg  13393  imasmulr  13394  subm0  13567  lssvancl1  14384  lssvnegcl  14393  lspprvacl  14430  lspsneli  14432  lspsn  14433  znf1o  14668  ntrin  14851  topssnei  14889  restbasg  14895  cnntri  14951  txcn  15002  txlm  15006  cnmpt2res  15024  psmetlecl  15061  xmetlecl  15094  bldisj  15128  bdmet  15229  bdbl  15230  bdmopn  15231  xmetxp  15234  metcnp  15239  tgioo  15281  cncfmet  15319  dedekindeulemlub  15347  suplociccreex  15351  ellimc3apf  15387  limcimolemlt  15391  limccnp2cntop  15404  dvfvalap  15408  dvidsslem  15420  dvmulxxbr  15429  dvaddxx  15430  dvmulxx  15431  dviaddf  15432  dvimulf  15433  dvcoapbr  15434  dvmptclx  15445  cxplt3  15647  cxpltd  15655  cxpled  15656  cxplt3d  15662  cxple3d  15663  logbrec  15687  logbgcd1irraplemap  15696  wilthlem1  15707  mpodvdsmulf1o  15717  lgslem1  15732  lgslem3  15734  lgsdirprm  15766  gausslemma2dlem1f1o  15792  gausslemma2dlem6  15799  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem4  15805  lgseisen  15806  lgsquadlem1  15809  lgsquad2lem1  15813  lgsquad3  15816  m1lgs  15817  2lgslem1a1  15818  2sqlem7  15853  usgredg2v  16078  vtxd0nedgbfi  16153  clwwlknonex2  16293  gsumgfsumlem  16704  gfsump1  16707