Theorem syl22anc 1275

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 1272	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  5665  tfrexlem  6578  th3qlem1  6884  en2prd  7072  enpr2d  7077  ssenen  7118  phplem4dom  7129  phplem4on  7135  fiunsnnn  7151  findcard2sd  7162  unsnfi  7192  sbthlemi9  7248  fsuppcorn  7267  endjusym  7400  endjudisj  7530  djuen  7531  ltanqg  7731  ltmnqg  7732  ltnnnq  7754  addcmpblnq0  7774  addlocprlemeqgt  7863  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  addcanprleml  7945  recexprlem1ssl  7964  caucvgprlemloc  8006  caucvgprprlemloccalc  8015  mulcmpblnr  8072  ltasrg  8101  recexgt0sr  8104  mulextsr1lem  8111  mulextsr1  8112  srpospr  8114  prsrlt  8118  ltpsrprg  8134  mappsrprg  8135  pitonnlem1p1  8177  recidpirq  8189  axpre-ltadd  8217  mulgt0d  8413  mul4d  8445  add4d  8459  add42d  8460  subcan  8545  addsub4d  8648  subadd4d  8649  sub4d  8650  2addsubd  8651  addsubeq4d  8652  muladdd  8707  mulsubd  8708  addgegt0d  8811  addgtge0d  8812  addge0d  8814  le2addd  8855  le2subd  8856  ltleaddd  8857  leltaddd  8858  lt2subd  8860  apreap  8879  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  mulap0r  8907  mulge0d  8913  mulap0d  8950  divdivdivap  9007  divcanap5  9008  divap0d  9100  recdivapd  9101  recdivap2d  9102  divcanap6d  9103  ddcanapd  9104  rec11apd  9105  divmuldivapd  9126  divmuleqapd  9127  subrecapd  9135  prodgt0  9146  lt2msq  9180  ledivdiv  9184  lediv12a  9188  recreclt  9194  divgt0d  9229  mulgt1d  9230  lemulge11d  9231  lemulge12d  9232  ltmul12ad  9235  lemul12ad  9236  lemul12bd  9237  nndivtr  9299  qreccl  9995  ledivdivd  10076  lediv12ad  10110  lt2mul2divd  10119  xlt2add  10235  xleaddadd  10242  iccss2  10299  iccssico2  10302  lincmb01cmp  10358  iccf1o  10360  fzrev2i  10445  qtri3or  10627  elicore  10653  2tnp1ge0ge0  10688  modqid  10738  q0mod  10744  q1mod  10745  modqabs  10746  modqadd1  10750  mulqaddmodid  10753  mulp1mod1  10754  modqmuladd  10755  modqmuladdnn0  10757  qnegmod  10758  m1modnnsub1  10759  addmodid  10761  modqm1p1mod0  10764  modqltm1p1mod  10765  modqmul1  10766  q2submod  10774  modifeq2int  10775  modaddmodup  10776  modaddmodlo  10777  modqaddmulmod  10780  modqsubdir  10782  modqeqmodmin  10783  modsumfzodifsn  10785  addmodlteq  10787  frecfzennn  10815  ser3mono  10876  expcl2lemap  10940  mulexpzap  10968  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  ltexp2a  10980  leexp2a  10981  sqdivap  10992  qsqeqor  11039  expnbnd  11053  expsubapd  11074  lt2sqd  11094  le2sqd  11095  sq11d  11096  apexp1  11108  bcp1nk  11152  hashunlem  11196  zfz1isolem1  11240  hashtpgim  11245  cjap  11619  cnreim  11691  resqrexlem1arp  11718  resqrexlemp1rp  11719  resqrexlemglsq  11735  abs00ap  11775  absext  11776  absexpzap  11793  absrele  11796  sqrtmuld  11882  sqrtsq2d  11883  sqrtled  11884  sqrtltd  11885  sqr11d  11886  abs3lemd  11914  minmax  11943  xrmaxiflemlub  11961  xrltmaxsup  11970  xrminmax  11978  xrbdtri  11989  climuni  12006  2clim  12014  addcn2  12023  mulcn2  12025  fsum3  12101  mptfzshft  12156  fsumrev  12157  fisum0diag2  12161  modfsummodlemstep  12171  binomlem  12197  mertenslemi1  12249  fprodrev  12333  efcllemp  12372  p1modz1  12508  dvds1  12567  dvdsext  12569  mulmoddvds  12577  oexpneg  12591  evennn02n  12596  evennn2n  12597  bitsinv1  12676  bezoutlemmo  12730  mulgcd  12740  dvdssqlem  12754  rpmulgcd2  12820  isprm6  12872  sqrt2irraplemnn  12904  sqrt2irrap  12905  crth  12949  eulerthlemh  12956  prmdiveq  12961  powm2modprm  12978  modprm0  12980  pythagtriplem2  12992  pythagtriplem11  13000  pythagtriplem13  13002  pythagtrip  13009  pcid  13050  pcgcd1  13054  pcprmpw2  13059  dvdsprmpweqle  13063  pcaddlem  13065  pcadd  13066  fldivp1  13074  4sqlem12  13128  4sqlem14  13130  4sqlem15  13131  4sqlem16  13132  ballotfilemsima  13206  ballotfilemfrceq  13219  unennn  13235  ennnfonelemg  13241  ennnfonelemhf1o  13251  inffinp1  13267  isstructr  13314  setscomd  13340  imasbas  13574  imasplusg  13575  imasmulr  13576  subm0  13740  gsumshift  14108  gfsump1  14111  lssvancl1  14644  lssvnegcl  14653  lspprvacl  14690  lspsneli  14692  lspsn  14693  znf1o  14928  ntrin  15118  topssnei  15156  restbasg  15162  cnntri  15218  txcn  15269  txlm  15273  cnmpt2res  15291  psmetlecl  15328  xmetlecl  15361  bldisj  15395  bdmet  15496  bdbl  15497  bdmopn  15498  xmetxp  15501  metcnp  15506  tgioo  15548  cncfmet  15586  dedekindeulemlub  15614  suplociccreex  15618  ellimc3apf  15654  limcimolemlt  15658  limccnp2cntop  15671  dvfvalap  15675  dvidsslem  15687  dvmulxxbr  15696  dvaddxx  15697  dvmulxx  15698  dviaddf  15699  dvimulf  15700  dvcoapbr  15701  dvmptclx  15712  cxplt3  15914  cxpltd  15922  cxpled  15923  cxplt3d  15929  cxple3d  15930  logbrec  15954  logbgcd1irraplemap  15963  pellexlem1  15974  pellexlem2  15975  wilthlem1  15977  mpodvdsmulf1o  15987  lgslem1  16002  lgslem3  16004  lgsdirprm  16036  gausslemma2dlem1f1o  16062  gausslemma2dlem6  16069  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem4  16075  lgseisen  16076  lgsquadlem1  16079  lgsquad2lem1  16083  lgsquad3  16086  m1lgs  16087  2lgslem1a1  16088  2sqlem7  16123  usgredg2v  16348  vtxd0nedgbfi  16423  clwwlknonex2  16563