Theorem sylan2b 606

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	⊢ (𝜑 ↔ 𝜒)
sylan2b.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2b	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 ⊢ (𝜑 ↔ 𝜒)
2	1	biimpi 219	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 605	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ 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:  syl2anb  610  eupickb  2661  2eu1  2676  2eu1v  2677  elnelne1  3073  elnelne2  3074  morex  3677  psssstr  4058  reuss2  4272  reupick  4275  reximdva0  4303  falseral0OLD  4471  rabsneu  4690  invdisjrab  5090  opabss  5169  triun  5227  triin  5229  poirr  5571  wefrc  5645  xpcan  6168  fnfco  6745  eqfnun  7034  fnressn  7160  fvtp3  7200  fvtp3g  7203  f1mpt  7263  offval  7700  ordsucuniel  7833  onzsl  7855  soex  7931  fiunlem  7952  fiun  7953  f1iun  7954  dfoprab3  8063  poxp  8138  fnwelem  8141  poxp2  8153  suppssr  8205  suppssrg  8206  suppsssn  8211  suppofssd  8213  fprlem2  8312  oeordsuc  8596  oelim2  8597  omsmolem  8659  ssnnfi  9178  ssfi  9181  ensymfib  9192  domnsymfi  9208  fiint  9311  unifi  9326  indexfi  9342  iinfi  9402  unwdomg  9571  inf3lem5  9626  rankr1bg  9804  rankr1c  9823  elhf4  9905  carden2a  10040  dfac8clem  10104  dfac5lem4  10198  pwsdompw  10274  cfsuc  10328  cflim2  10334  enfin2i  10392  isf34lem4  10448  axdc4lem  10526  zornn0g  10576  uniimadomf  10622  fpwwe2lem7  10715  fpwwe2lem11  10719  fpwwe2lem12  10720  pwfseqlem1  10736  pwfseqlem5  10741  intgru  10892  addclpi  10970  addnidpi  10979  ltsonq  11047  nqpr  11092  reclem3pr  11127  recexsr  11185  supsrlem  11189  nnnn0addcl  12629  un0addcl  12632  un0mulcl  12633  nn0nndivcl  12671  nn0ge0div  12761  uzind3  12786  uzind4  13026  zsupss  13057  rpnnen1lem2  13098  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  ltsubrp  13151  ltaddrp  13152  xrlttr  13262  qbtwnxr  13323  xltnegi  13339  xaddnemnf  13359  xaddnepnf  13360  xaddcom  13363  xnegdi  13371  xsubge0  13384  xrub  13435  fzne1  13731  fzind2  13916  seqof  14195  expp1  14204  expneg  14205  expcllem  14208  mulexpz  14238  expaddz  14242  expmulz  14244  faclbnd4lem3  14432  faclbnd4  14434  fi1uzind  14645  swrd00  14785  swrd0  14801  cats1un  14863  reuccatpfxs1  14889  cshw0  14938  cshwn  14941  wwlktovfo  15104  shftf  15225  sqrtdiv  15425  leabs  15459  mulcn2  15756  summolem2  15875  fsumrev2  15941  geomulcvg  16038  prodmolem2  16095  zprod  16097  prodsn  16122  prodsnf  16124  fprodle  16156  bpolydiflem  16213  bpoly2  16216  bpoly3  16217  ruclem6  16396  dvdsflip  16480  dvdsfac  16489  gcdcllem1  16662  lcmgcdlem  16774  rpexp1i  16892  hashdvds  16945  hashgcdlem  16958  phisum  16961  iserodd  17006  pcqcl  17027  pcid  17044  ismred  17765  funcpropd  18070  natpropd  18147  odupos  18493  lubun  18682  rabsubmgmd  18886  sgrpidmnd  18921  issubmd  18994  grpinvnzcl  19214  mulgneg  19295  mulgnn0z  19304  symgfixf1  19644  symgsssg  19674  symgfisg  19675  pgpssslw  19821  sylow2alem2  19825  sylow2a  19826  oddvdssubg  20062  gsumzunsnd  20163  gsumunsnfd  20164  gsum2dlem1  20177  gsum2dlem2  20178  gsumcom3  20185  ablfac1eu  20282  pgpfac1lem5  20288  gsumdixp  20541  dvdsrcl2  20589  01eq0ring  20774  isdrng3lem1  20998  isdrng3lem2  20999  isdrngd  21015  isdrngdOLD  21017  unichnlidl  21509  isprmidlc  21621  ssdifidllem  21633  ssdifidlprm  21635  cnsubrg  21726  psgnodpm  21887  evlslem4  22378  psdmul  22480  coe1tmmul2  22588  mpomatmul  22754  matunitlindflem1  22987  cpmidpmat  23184  intcld  23351  neiptopnei  23443  ordtrest2lem  23514  lmss  23609  cmpcovf  23702  cncmp  23703  fincmp  23704  cmpsublem  23710  cmpsub  23711  unconn  23740  1stcfb  23756  2ndcsep  23771  refun0  23827  locfincmp  23838  1stckgenlem  23865  ptbasin  23889  ptbasfi  23893  ptunimpt  23907  ptuniconst  23910  dfac14  23930  ptcnp  23934  xkoptsub  23966  xkococnlem  23971  xkoinjcn  23999  qtopcmplem  24019  qtophmeo  24129  fbfinnfr  24153  isufil2  24220  isfcls  24321  xmetrtri  24667  xmetrtri2  24668  blssioo  25107  divcn  25182  bndth  25272  clmvscom  25404  resscdrg  25672  minveclem3  25743  finiunmbl  25858  opnmbllem  25915  ismbf2d  25954  itg2seq  26056  bddiblnc  26155  ellimc2  26190  limcmpt2  26197  limcres  26199  dvlem  26209  dvidlem  26228  dvrec  26268  dveflem  26292  dvlip  26306  coe1mul3  26410  dvtaylp  26690  leibpilem2  27262  leibpi  27263  wilthlem2  27389  basellem3  27403  dchreq  27578  dchrsum  27589  lgsval3  27635  lgsdir2lem4  27648  2sqlem6  27743  rpvmasumlem  27807  dchrisum0fno1  27831  rpvmasum2  27832  pntrsumbnd2  27887  ostthlem1  27947  infdesc  27960  nosupno  28053  negbdaylem  28435  expsp1  28808  colmid  29153  plngrotlem2  29259  lmiisolem  29294  dfcgra2  29331  prlngmolem2  29424  axcontlem2  29536  axcontlem7  29541  upgrex  29663  umgredg  29709  umgrpredgv  29711  umgredgne  29716  umgredgnlp  29718  usgredgppr  29770  edgssv2  29772  uspgredg2vlem  29797  usgredg2vlem1  29799  upgrres1  29887  nbuhgr2vtx1edgblem  29925  nbusgrf1o0  29943  hashnbusgrnn0  29950  iscplgredg  29991  uhgrvd00  30108  finsumvtxdg2size  30124  wlkepvtx  30232  wlknewwlksn  30469  wwlksnextfun  30480  wwlksnextsurj  30482  elwwlks2ons3im  30536  wwlks2onsym  30542  clwwlkf  30631  fusgreghash2wspv  30929  numclwwlk5lem  30981  grpoidinvlem3  31101  ablo32  31144  ablomuldiv  31147  ablodivdiv  31148  ablodiv32  31150  nvscom  31224  dipassr  31441  htthlem  31512  hsn0elch  31843  shscli  31912  nmopun  32609  branmfn  32700  mdslj1i  32914  mdslj2i  32915  atss  32941  chcv1  32950  dmdbr5ati  33017  snsssng  33103  ifnebib  33138  fnpreimac  33257  fcnvgreu  33259  isoun  33288  fsuppcurry1  33309  fsuppcurry2  33310  prodpr  33410  prodtp  33411  pmtrprfv2  33642  elrgspnsubrunlem2  33802  nsgmgclem  33955  nsgqusf1olem2  33958  ssmxidllem  33991  qsdrng  34014  1arithufdlem3  34071  ordtrest2NEWlem  34547  esumsplit  34678  esumpad2  34681  esumpcvgval  34703  sigaclcu2  34745  ldgenpisyslem1  34789  volmeas  34857  mbfmco2  34890  omsmeas  34948  oddpwdc  34979  eulerpartlemgvv  35001  ballotlemfc0  35118  ballotlemfcc  35119  prodfzo03  35225  circlemethhgt  35265  bnj1109  35410  bnj1294  35440  bnj545  35518  bnj605  35530  bnj594  35535  bnj934  35558  bnj953  35562  bnj1137  35618  bnj1174  35626  bnj1388  35656  vonf1oonfo  35877  subfacp1lem4  35927  erdszelem7  35941  erdszelem8  35942  erdsze2lem2  35948  resconn  35990  cvmsdisj  36014  cvmscld  36017  satf0op  36121  mclsax  36313  climuzcnv  36415  pocnv  36507  cgrid2  36748  btwncom  36759  btwnswapid2  36763  colinearperm1  36807  colinearperm3  36808  colinearperm2  36809  colinearperm4  36810  lineext  36821  colinbtwnle  36863  broutsideof2  36867  outsideofcom  36873  linecom  36895  linerflx2  36896  lineintmo  36902  fwddifn0  36909  hfext  36914  nmulel1  36944  ntruni  37095  clsint2  37097  neibastop1  37127  weiunlem  37231  bj-snsetex  37856  relowlssretop  38266  pibt2  38320  fin2solem  38509  lindsadd  38516  poimirlem4  38522  poimirlem25  38543  poimirlem32  38550  opnmbllem0  38554  mblfinlem3  38557  mbfposadd  38565  itg2addnclem3  38571  ftc1anclem6  38596  ftc1anc  38599  ac6gf  38646  heibor1lem  38723  isdrngo2  38872  unichnidl  38945  isfldidl  38982  cnf1dd  39002  membpartlem19  39826  lkrss2N  40206  elpadd0  40846  ltrnu  41158  tendoex  42012  cdlemm10N  42155  dicfnN  42220  dihmeetlem2N  42336  dihlatat  42374  lcfrlem9  42587  uzindd  43008  sticksstones1  43176  ofun  43269  nn0addcom  43506  nn0mulcom  43510  zmulcomlem  43511  fsuppind  43598  ismrcd1  43688  isnacs3  43700  pellfundglb  43871  jm2.22  43981  jm2.23  43982  isnumbasgrplem1  44087  hbtlem6  44115  rngunsnply  44155  ordsssucim  44388  mnringmulrcld  45211  dvgrat  45281  cvgdvgrat  45282  nznngen  45285  uzmptshftfval  45315  wfac8prim  45970  rnmptlb  46224  rnmptbddlem  46225  rnmptbd2lem  46229  iccshift  46499  iooshift  46503  liminflbuz2  46794  xlimbr  46806  itgperiod  46960  fourierdlem42  47128  fourierdlem68  47153  fourierdlem93  47178  smfpimne2  47819  elprneb  48068  dfatcolem  48294  modmknepk  48407  ichim  48508  ichnfb  48516  prproropf1olem1  48554  prproropf1olem3  48556  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  2zlidl  49306  lspsslco  49518  isthincd2  50514  fullthinc  50527