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  5662  tfrexlem  6567  th3qlem1  6873  en2prd  7061  enpr2d  7066  ssenen  7107  phplem4dom  7118  phplem4on  7124  fiunsnnn  7140  findcard2sd  7151  unsnfi  7181  sbthlemi9  7237  fsuppcorn  7256  endjusym  7389  endjudisj  7519  djuen  7520  ltanqg  7720  ltmnqg  7721  ltnnnq  7743  addcmpblnq0  7763  addlocprlemeqgt  7852  distrlem1prl  7902  distrlem1pru  7903  distrlem4prl  7904  distrlem4pru  7905  addcanprleml  7934  recexprlem1ssl  7953  caucvgprlemloc  7995  caucvgprprlemloccalc  8004  mulcmpblnr  8061  ltasrg  8090  recexgt0sr  8093  mulextsr1lem  8100  mulextsr1  8101  srpospr  8103  prsrlt  8107  ltpsrprg  8123  mappsrprg  8124  pitonnlem1p1  8166  recidpirq  8178  axpre-ltadd  8206  mulgt0d  8401  mul4d  8433  add4d  8447  add42d  8448  subcan  8533  addsub4d  8636  subadd4d  8637  sub4d  8638  2addsubd  8639  addsubeq4d  8640  muladdd  8694  mulsubd  8695  addgegt0d  8798  addgtge0d  8799  addge0d  8801  le2addd  8842  le2subd  8843  ltleaddd  8844  leltaddd  8845  lt2subd  8847  apreap  8866  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  mulap0r  8894  mulge0d  8900  mulap0d  8937  divdivdivap  8992  divcanap5  8993  divap0d  9085  recdivapd  9086  recdivap2d  9087  divcanap6d  9088  ddcanapd  9089  rec11apd  9090  divmuldivapd  9111  divmuleqapd  9112  subrecapd  9120  prodgt0  9131  lt2msq  9165  ledivdiv  9169  lediv12a  9173  recreclt  9179  divgt0d  9214  mulgt1d  9215  lemulge11d  9216  lemulge12d  9217  ltmul12ad  9220  lemul12ad  9221  lemul12bd  9222  nndivtr  9284  qreccl  9980  ledivdivd  10061  lediv12ad  10095  lt2mul2divd  10104  xlt2add  10219  xleaddadd  10226  iccss2  10283  iccssico2  10286  lincmb01cmp  10342  iccf1o  10344  fzrev2i  10427  qtri3or  10607  elicore  10633  2tnp1ge0ge0  10668  modqid  10718  q0mod  10724  q1mod  10725  modqabs  10726  modqadd1  10730  mulqaddmodid  10733  mulp1mod1  10734  modqmuladd  10735  modqmuladdnn0  10737  qnegmod  10738  m1modnnsub1  10739  addmodid  10741  modqm1p1mod0  10744  modqltm1p1mod  10745  modqmul1  10746  q2submod  10754  modifeq2int  10755  modaddmodup  10756  modaddmodlo  10757  modqaddmulmod  10760  modqsubdir  10762  modqeqmodmin  10763  modsumfzodifsn  10765  addmodlteq  10767  frecfzennn  10795  ser3mono  10856  expcl2lemap  10920  mulexpzap  10948  expaddzaplem  10951  expaddzap  10952  expmulzap  10954  ltexp2a  10960  leexp2a  10961  sqdivap  10972  qsqeqor  11019  expnbnd  11033  expsubapd  11054  lt2sqd  11074  le2sqd  11075  sq11d  11076  apexp1  11088  bcp1nk  11132  hashunlem  11176  zfz1isolem1  11220  hashtpgim  11225  cjap  11599  cnreim  11671  resqrexlem1arp  11698  resqrexlemp1rp  11699  resqrexlemglsq  11715  abs00ap  11755  absext  11756  absexpzap  11773  absrele  11776  sqrtmuld  11862  sqrtsq2d  11863  sqrtled  11864  sqrtltd  11865  sqr11d  11866  abs3lemd  11894  minmax  11923  xrmaxiflemlub  11941  xrltmaxsup  11950  xrminmax  11958  xrbdtri  11969  climuni  11986  2clim  11994  addcn2  12003  mulcn2  12005  fsum3  12081  mptfzshft  12136  fsumrev  12137  fisum0diag2  12141  modfsummodlemstep  12151  binomlem  12177  mertenslemi1  12229  fprodrev  12313  efcllemp  12352  p1modz1  12488  dvds1  12547  dvdsext  12549  mulmoddvds  12557  oexpneg  12571  evennn02n  12576  evennn2n  12577  bitsinv1  12656  bezoutlemmo  12710  mulgcd  12720  dvdssqlem  12734  rpmulgcd2  12800  isprm6  12852  sqrt2irraplemnn  12884  sqrt2irrap  12885  crth  12929  eulerthlemh  12936  prmdiveq  12941  powm2modprm  12958  modprm0  12960  pythagtriplem2  12972  pythagtriplem11  12980  pythagtriplem13  12982  pythagtrip  12989  pcid  13030  pcgcd1  13034  pcprmpw2  13039  dvdsprmpweqle  13043  pcaddlem  13045  pcadd  13046  fldivp1  13054  4sqlem12  13108  4sqlem14  13110  4sqlem15  13111  4sqlem16  13112  unennn  13169  ennnfonelemg  13175  ennnfonelemhf1o  13185  inffinp1  13201  isstructr  13248  setscomd  13274  imasbas  13541  imasplusg  13542  imasmulr  13543  subm0  13716  lssvancl1  14564  lssvnegcl  14573  lspprvacl  14610  lspsneli  14612  lspsn  14613  znf1o  14848  ntrin  15038  topssnei  15076  restbasg  15082  cnntri  15138  txcn  15189  txlm  15193  cnmpt2res  15211  psmetlecl  15248  xmetlecl  15281  bldisj  15315  bdmet  15416  bdbl  15417  bdmopn  15418  xmetxp  15421  metcnp  15426  tgioo  15468  cncfmet  15506  dedekindeulemlub  15534  suplociccreex  15538  ellimc3apf  15574  limcimolemlt  15578  limccnp2cntop  15591  dvfvalap  15595  dvidsslem  15607  dvmulxxbr  15616  dvaddxx  15617  dvmulxx  15618  dviaddf  15619  dvimulf  15620  dvcoapbr  15621  dvmptclx  15632  cxplt3  15834  cxpltd  15842  cxpled  15843  cxplt3d  15849  cxple3d  15850  logbrec  15874  logbgcd1irraplemap  15883  pellexlem1  15894  pellexlem2  15895  wilthlem1  15897  mpodvdsmulf1o  15907  lgslem1  15922  lgslem3  15924  lgsdirprm  15956  gausslemma2dlem1f1o  15982  gausslemma2dlem6  15989  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem4  15995  lgseisen  15996  lgsquadlem1  15999  lgsquad2lem1  16003  lgsquad3  16006  m1lgs  16007  2lgslem1a1  16008  2sqlem7  16043  usgredg2v  16268  vtxd0nedgbfi  16343  clwwlknonex2  16483  gsumgfsumlem  16914  gfsump1  16917