Theorem syl2an2r 698

Description: syl2anr 609 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)

Hypotheses

Ref	Expression
syl2an2r.1	⊢ (𝜑 → 𝜓)
syl2an2r.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)
syl2an2r.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl2an2r	⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Proof of Theorem syl2an2r

Step	Hyp	Ref	Expression
1		syl2an2r.2	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2		syl2an2r.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an2r.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	2, 3	sylan 592	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 603	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5111  axprlem4OLD  5406  brcogw  5859  funfni  6648  f1un  6848  fvelimab  6960  dff3  7102  fnex  7222  ralima  7242  f1cofveqaeq  7262  f1eqcocnv  7310  caofid0l  7720  caofid0r  7721  caofid1  7722  caofid2  7723  onmindif2  7815  limsssuc  7855  mptcnfimad  7992  fnse  8138  frrlem13  8304  iinon  8336  smoord  8361  smoword  8362  tfrlem11  8384  coflton  8666  cofonr  8669  naddasslem2  8691  boxcutc  8948  f1domg  8977  phpeqd  9206  ominf  9234  f1finf1o  9243  unfilem1  9275  f1opwfi  9323  marypha2  9409  supmax  9438  infmin  9466  ordtypelem6  9495  oiexg  9507  oien  9510  cantnff  9653  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1  9668  ttrcltr  9695  ttrclselem2  9705  opwf  9794  rankopb  9834  xpnum  9956  infxpenlem  10016  infxp  10216  cflim2  10265  cofsmo  10271  cfsmolem  10272  cfcoflem  10274  ssfin3ds  10332  isf34lem5  10380  isf34lem6  10382  isfin1-3  10388  axcc3  10440  alephval2  10575  fpwwe2lem7  10640  canthp1  10657  tsken  10757  ltaddpr  11037  dedekind  11391  recextlem2  11863  recex  11864  gt0div  12099  ge0div  12100  lerec2  12121  uzwo2  12954  infssuzcl  12974  qmulcl  13009  xnegdi  13292  xmulpnf1n  13322  xadddi2  13341  fzm1  13654  2submod  13988  addmodlteq  14002  expnlbnd  14289  faclbnd5  14354  hasheni  14404  hashdifpr  14472  hashgt23el  14481  ccatrn  14647  ccatf1  14648  ccatalpha  14652  swrds1  14728  swrdccat2  14731  ccatpfx  14762  swrdccatin2  14790  pfxccatin12lem2  14792  revccat  14827  revrev  14828  swrdco  14900  relexpindlem  15126  resqrex  15327  fzomaxdiflem  15420  climconst  15620  serf0  15758  fsumf1o  15800  fsumrev  15856  fsumabs  15879  cvgcmp  15894  binomlem  15909  isumshft  15919  climcndslem1  15929  climcndslem2  15930  climcnds  15931  supcvg  15936  fprodcl2lem  16030  tanneg  16229  rpnnen2lem11  16305  modm1div  16347  fzo0dvdseq  16406  bitsfzolem  16517  gcdcllem3  16584  hashdvds  16859  prmdivdiv  16871  reumodprminv  16889  nnnn0modprm0  16891  pythagtrip  16919  dvdsprmpweqle  16971  pockthg  16991  4sqlem9  17031  vdwmc2  17064  vdwlem2  17067  imasaddflem  17609  acsfn1  17742  acsfn1c  17743  acsfn2  17744  oppccofval  17797  rescabs  17915  diag2  18326  grpinvalem  18757  issubmnd  18848  imasmnd  18864  pwsco2mhm  18923  gsumwspan  18936  frmdss2  18953  grpinvssd  19114  pwssub  19151  imasgrp  19153  subginv  19230  subginvcl  19232  ecqusaddcl  19295  ghmpreima  19339  conjnsg  19355  gass  19402  gsmsymgreqlem2  19532  f1omvdmvd  19544  symgsssg  19568  symgfisg  19569  symgtrinv  19573  psgnunilem5  19595  sylow1lem2  19700  odcau  19705  sylow2a  19720  sylow2  19727  efgsp1  19838  frgpuptf  19871  frgpuptinv  19872  frgpupf  19874  frgpup3lem  19878  mulgdi  19927  gsumval3eu  20005  gsumzsplit  20028  gsumzmhm  20038  gsumxp2  20081  prdsgsum  20082  fsfnn0gsumfsffz  20084  ablfaclem3  20190  srgbinomlem  20343  gsummgp0  20432  pwsgprod  20444  imasring  20445  dvdsr01  20486  rngisom1  20581  01eq0ring  20665  issubrng2  20694  subrgcrng  20711  subrginv  20724  isdrngd  20905  imadrhmcl  20937  abv1z  20964  lcomfsupp  21060  lmodvneg1  21063  lspsn  21160  lmhmco  21201  lmhmima  21205  lmhmpreima  21206  reslmhm  21210  lbsextlem2  21320  isridlrng  21381  lidl0cl  21382  lidlunin0  21398  rspvalint  21406  elrspsn  21408  rnglidlmmgm  21416  rnglidlmsgrp  21417  2idlcpblrng  21447  quscrng  21460  rngqiprngghmlem1  21464  rngqiprngghmlem3  21466  rngqiprnglinlem3  21470  rngqiprngimf1lem  21471  rngqiprngimf  21474  rng2idl1cntr  21482  qsidomlem1  21517  qsidomlem2  21518  ssdifidllem  21521  ssdifidlprm  21523  znfld  21747  ipassr2  21834  ocvin  21861  pjfo  21902  obsne0  21912  frlmgsum  21959  aspval2  22085  psrlinv  22142  mplsubglem  22185  mpllsslem  22186  evlslem4  22264  evlslem1  22270  evlsval3  22277  mpfind  22303  evls1rhm  22519  madetsumid  22655  scmatcrng  22715  mdetleib2  22782  cramerimplem1  22877  m2pmfzgsumcl  22942  decpmatmul  22966  pmatcollpwscmat  22985  idpm2idmp  22995  pm2mpmhmlem1  23012  chpscmatgsummon  23039  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  topbas  23166  uncld  23235  incld  23237  elcls  23267  neiptopnei  23326  resttopon  23355  restdis  23372  cnclima  23462  paste  23488  cncmp  23586  clsconn  23624  conncompcld  23628  1stcfb  23639  2ndcsb  23643  2ndcredom  23644  kgencmp2  23740  txss12  23799  qtoptop2  23893  qtoptopon  23898  hmphindis  23991  uffixfr  24117  ufildr  24125  isfcls2  24207  tgplacthmeo  24297  tsmsgsum  24333  tgptsmscld  24345  tsmssplit  24346  ustuqtop5  24439  uspreg  24467  prdsxmetlem  24562  prdsbl  24685  metss  24702  metrest  24718  nrmmetd  24768  isngp2  24791  ngpsubcan  24808  lssnlm  24895  nmoid  24936  opnreen  25026  mpomulcn  25063  evth  25155  htpyco2  25175  phtpyco2  25186  clmvz  25307  tcphcph  25433  iscmet3  25489  metcld  25502  bcthlem2  25521  cssbn  25571  chlcsschl  25574  minveclem1  25620  evthicc2  25656  ovolunlem1a  25692  ovolicc2lem1  25713  ovolicc2lem4  25716  ovolicc2lem5  25717  uniioombllem2  25779  uniioombllem3  25781  vitalilem2  25805  vitalilem4  25807  vitalilem5  25808  itg2monolem1  25946  cpnres  26133  rolle  26186  dvlip2  26191  dvivthlem2  26205  dvfsumrlimge0  26226  deg1pwle  26314  plydivlem4  26494  ulm0  26591  efif1olem1  26744  efif1olem2  26745  eflogeq  26804  argimlt0  26815  logrec  26965  relogbcxp  26987  atanlogadd  27116  atanlogsub  27118  atantan  27125  ftalem4  27277  ftalem5  27278  basellem3  27284  chtub  27413  dchrpt  27468  dchrsum2  27469  gausslemma2dlem1a  27566  2lgslem3a1  27601  2lgslem3b1  27602  2lgslem3c1  27603  2lgslem3d1  27604  2lgsoddprm  27617  dchrisumlem2  27691  pntrsumbnd2  27768  nosupbnd1lem4  27912  noinfbnd2lem1  27931  cutbdaylt  28028  oldlim  28117  madebday  28130  cofcutr  28154  addbday  28248  negbdaylem  28286  absmuls  28474  absnegs  28477  bdayfinlem  28716  cnvmot  28847  tglineneq  28955  midexlem  29006  midex  29055  plngrotlem1  29106  axlowdimlem14  29342  uhgrspansubgrlem  29677  usgrres  29695  usgrnbcnvfv  29752  finsumvtxdg2sstep  29936  uspgr2wlkeq  30032  redwlk  30057  pthdivtx  30113  usgr2wlkspthlem2  30144  wwlknvtx  30231  2wlkdlem6  30317  umgr2wlkon  30336  rusgrnumwwlk  30364  clwwlkwwlksb  30442  clwwlknwwlksnb  30443  clwwnisshclwwsn  30447  clwwlknscsh  30450  clwlknf1oclwwlknlem1  30469  1wlkdlem2  30526  fusgreghash2wsp  30726  2clwwlklem  30731  2clwwlk2clwwlk  30738  numclwwlk6  30778  prssad  32912  prssbd  32913  ofrn2  33022  ofpreima2  33048  sgnval2  33117  argcj  33130  wrdsplex  33293  mgcf1o  33354  gsumfs2d  33412  gsumhashmul  33418  gsummulsubdishift1  33419  cycpmco2lem5  33481  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmco2  33484  cyc3co2  33491  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnsubrunlem1  33598  erler  33616  fracerl  33658  imaslmod  33704  elrspunidl  33767  ressply1evls1  33886  ply1coedeg  33910  esplyfval3  33993  exsslsb  34018  dimpropd  34030  lbsdiflsp0  34047  extdg1id  34087  madjusmdetlem2  34249  zarcmplem  34302  eulerpartlemgvv  34798  boolesineq  34877  fineqvnttrclselem1  35558  vonf1wev  35616  vonf1owevOLD  35618  pfxwlk  35637  revwlk  35638  pthhashvtx  35641  spthcycl  35642  umgracycusgr  35667  subfacp1lem5  35697  satfvsucsuc  35878  ply1divalg3  36155  weiunfrlem  37016  ttctr  37045  dfttc2g  37058  cnambfre  38360  mapdordlem2  42452  frlmvscadiccat  43321  ricdrng1  43337  evlsbagval  43359  0prjspn  43401  3cubes  43462  oninfint  44004  onexomgt  44009  onexoegt  44012  ordeldif  44026  oacl2g  44098  onmcl  44099  omabs2  44100  omcl2  44101  tfsconcatfv  44109  tfsconcatrev  44116  ofoafg  44122  ofoafo  44124  ofoaass  44128  ofoacom  44129  onsucunifi  44138  oaun3lem1  44142  oadif1lem  44147  oadif1  44148  naddwordnexlem4  44169  safesnsupfilb  44185  gneispace  44901  rr-phpd  44974  grumnudlem  45036  ax6e2ndeqALT  45680  sineq0ALT  45686  hashnnlt  45772  fnresdmss  45927  saliinclf  47081  hoicvr  47303  setsv  48168  sprsymrelfolem2  48283  lighneal  48404  indprmfz  48423  grimuhgr  48693  grimcnv  48694  uhgrimedgi  48696  uhgrimedg  48697  isuspgrim0lem  48699  isuspgrim0  48700  upgrimtrlslem1  48710  upgrimtrlslem2  48711  clnbgrgrim  48740  grimedg  48741  isubgr3stgrlem8  48779  clnbgr3stgrgrlim  48825  clnbgr3stgrgrlic  48826  lincresunit3  49302  2itscp  49602  resccat  49893