Theorem sylan2b 593

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 215	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 592	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  syl2anb  597  eupickb  2637  2eu1  2652  2eu1v  2653  eqtr3OLD  2765  elnelne1  3058  elnelne2  3059  morex  3649  psssstr  4037  reuss2  4246  reupick  4249  reximdva0  4282  falseral0  4447  rabsneu  4662  invdisjrabw  5055  opabss  5134  triun  5200  triin  5202  poirr  5506  wefrc  5574  xpcan  6068  fnfco  6623  fnressn  7012  fvtp3  7054  fvtp3g  7057  f1mpt  7115  offval  7520  ordsucuniel  7646  onzsl  7668  soex  7742  fiunlem  7758  fiun  7759  f1iun  7760  dfoprab3  7867  poxp  7940  fnwelem  7943  suppssr  7983  suppssrg  7984  suppsssn  7988  suppofssd  7990  fprlem2  8088  oeordsuc  8387  oelim2  8388  omsmolem  8447  rexdif1en  8906  ssnnfi  8914  ssnnfiOLD  8915  ssfi  8918  ensymfib  8930  fiint  9021  unifi  9038  indexfi  9057  iinfi  9106  unwdomg  9273  inf3lem5  9320  trpredmintr  9409  rankr1bg  9492  rankr1c  9510  carden2a  9655  dfac8clem  9719  dfac5lem4  9813  pwsdompw  9891  cfsuc  9944  cflim2  9950  enfin2i  10008  isf34lem4  10064  axdc4lem  10142  zornn0g  10192  uniimadomf  10232  fpwwe2lem7  10324  fpwwe2lem11  10328  fpwwe2lem12  10329  pwfseqlem1  10345  pwfseqlem5  10350  intgru  10501  addclpi  10579  addnidpi  10588  ltsonq  10656  nqpr  10701  reclem3pr  10736  recexsr  10794  supsrlem  10798  nnnn0addcl  12193  un0addcl  12196  un0mulcl  12197  nn0nndivcl  12234  nn0ge0div  12319  uzind3  12344  uzind4  12575  zsupss  12606  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  ltsubrp  12695  ltaddrp  12696  xrlttr  12803  qbtwnxr  12863  xltnegi  12879  xaddnemnf  12899  xaddnepnf  12900  xaddcom  12903  xnegdi  12911  xsubge0  12924  xrub  12975  fzind2  13433  seqof  13708  expp1  13717  expneg  13718  expcllem  13721  mulexpz  13751  expaddz  13755  expmulz  13757  faclbnd4lem3  13937  faclbnd4  13939  fi1uzind  14139  swrd00  14285  swrd0  14299  cats1un  14362  reuccatpfxs1  14388  cshw0  14435  cshwn  14438  wwlktovfo  14601  shftf  14718  sqrtdiv  14905  leabs  14939  mulcn2  15233  summolem2  15356  fsumrev2  15422  geomulcvg  15516  prodmolem2  15573  zprod  15575  prodsn  15600  prodsnf  15602  fprodle  15634  bpolydiflem  15692  bpoly2  15695  bpoly3  15696  ruclem6  15872  dvdsflip  15954  dvdsfac  15963  gcdcllem1  16134  lcmgcdlem  16239  rpexp1i  16356  hashdvds  16404  hashgcdlem  16417  phisum  16419  iserodd  16464  pcqcl  16485  pcid  16502  ismred  17228  funcpropd  17532  natpropd  17610  odupos  17961  lubun  18148  sgrpidmnd  18305  issubmd  18360  grpinvnzcl  18562  mulgneg  18637  mulgnn0z  18645  symgfixf1  18960  symgsssg  18990  symgfisg  18991  pgpssslw  19134  sylow2alem2  19138  sylow2a  19139  oddvdssubg  19371  gsumzunsnd  19472  gsumunsnfd  19473  gsum2dlem1  19486  gsum2dlem2  19487  gsumcom3  19494  ablfac1eu  19591  pgpfac1lem5  19597  gsumdixp  19763  dvdsrcl2  19807  isdrngd  19931  cnsubrg  20570  psgnodpm  20705  evlslem4  21194  coe1tmmul2  21357  mpomatmul  21503  cpmidpmat  21930  intcld  22099  neiptopnei  22191  ordtrest2lem  22262  lmss  22357  cmpcovf  22450  cncmp  22451  fincmp  22452  cmpsublem  22458  cmpsub  22459  unconn  22488  1stcfb  22504  2ndcsep  22518  refun0  22574  locfincmp  22585  1stckgenlem  22612  ptbasin  22636  ptbasfi  22640  ptunimpt  22654  ptuniconst  22657  dfac14  22677  ptcnp  22681  xkoptsub  22713  xkococnlem  22718  xkoinjcn  22746  qtopcmplem  22766  qtophmeo  22876  fbfinnfr  22900  isufil2  22967  isfcls  23068  xmetrtri  23416  xmetrtri2  23417  blssioo  23864  divcn  23937  bndth  24027  clmvscom  24159  resscdrg  24427  minveclem3  24498  finiunmbl  24613  opnmbllem  24670  ismbf2d  24709  itg2seq  24812  bddiblnc  24911  ellimc2  24946  limcmpt2  24953  limcres  24955  dvlem  24965  dvidlem  24984  dvrec  25024  dveflem  25048  dvlip  25062  coe1mul3  25169  dvtaylp  25434  leibpilem2  25996  leibpi  25997  wilthlem2  26123  basellem3  26137  dchreq  26311  dchrsum  26322  lgsval3  26368  lgsdir2lem4  26381  2sqlem6  26476  rpvmasumlem  26540  dchrisum0fno1  26564  rpvmasum2  26565  pntrsumbnd2  26620  ostthlem1  26680  colmid  26953  lmiisolem  27061  dfcgra2  27095  axcontlem2  27236  axcontlem7  27241  upgrex  27365  umgredg  27411  umgrpredgv  27413  umgredgne  27418  umgredgnlp  27420  usgredgppr  27466  edgssv2  27468  uspgredg2vlem  27493  usgredg2vlem1  27495  upgrres1  27583  nbuhgr2vtx1edgblem  27621  nbusgrf1o0  27639  hashnbusgrnn0  27646  iscplgredg  27687  uhgrvd00  27804  finsumvtxdg2size  27820  wlkepvtx  27930  wlknewwlksn  28153  wwlksnextfun  28164  wwlksnextsurj  28166  elwwlks2ons3im  28220  wwlks2onsym  28224  clwwlkf  28312  fusgreghash2wspv  28600  numclwwlk5lem  28652  grpoidinvlem3  28769  ablo32  28812  ablomuldiv  28815  ablodivdiv  28816  ablodiv32  28818  nvscom  28892  dipassr  29109  htthlem  29180  hsn0elch  29511  shscli  29580  nmopun  30277  branmfn  30368  mdslj1i  30582  mdslj2i  30583  atss  30609  chcv1  30618  dmdbr5ati  30685  snsssng  30761  fnpreimac  30910  fcnvgreu  30912  isoun  30936  fsuppcurry1  30962  fsuppcurry2  30963  fzne1  31011  prodpr  31042  prodtp  31043  pmtrprfv2  31259  nsgmgclem  31498  nsgqusf1olem2  31501  isprmidlc  31525  ssmxidllem  31543  ordtrest2NEWlem  31774  esumsplit  31921  esumpad2  31924  esumpcvgval  31946  sigaclcu2  31988  ldgenpisyslem1  32031  volmeas  32099  mbfmco2  32132  omsmeas  32190  oddpwdc  32221  eulerpartlemgvv  32243  ballotlemfc0  32359  ballotlemfcc  32360  prodfzo03  32483  circlemethhgt  32523  bnj521  32616  bnj1109  32666  bnj1294  32697  bnj545  32775  bnj605  32787  bnj594  32792  bnj934  32815  bnj953  32819  bnj1137  32875  bnj1174  32883  bnj1388  32913  subfacp1lem4  33045  erdszelem7  33059  erdszelem8  33060  erdsze2lem2  33066  resconn  33108  cvmsdisj  33132  cvmscld  33135  satf0op  33239  mclsax  33431  climuzcnv  33529  pocnv  33636  poxp2  33717  nosupno  33833  cgrid2  34232  btwncom  34243  btwnswapid2  34247  colinearperm1  34291  colinearperm3  34292  colinearperm2  34293  colinearperm4  34294  lineext  34305  colinbtwnle  34347  broutsideof2  34351  outsideofcom  34357  linecom  34379  linerflx2  34380  lineintmo  34386  fwddifn0  34393  hfext  34412  ntruni  34443  clsint2  34445  neibastop1  34475  bj-snsetex  35080  relowlssretop  35461  pibt2  35515  fin2solem  35690  lindsadd  35697  matunitlindflem1  35700  poimirlem4  35708  poimirlem25  35729  poimirlem32  35736  opnmbllem0  35740  mblfinlem3  35743  mbfposadd  35751  itg2addnclem3  35757  ftc1anclem6  35782  ftc1anc  35785  eqfnun  35807  ac6gf  35817  heibor1lem  35894  isdrngo2  36043  unichnidl  36116  isfldidl  36153  cnf1dd  36175  lkrss2N  37110  elpadd0  37750  ltrnu  38062  tendoex  38916  cdlemm10N  39059  dicfnN  39124  dihmeetlem2N  39240  dihlatat  39278  lcfrlem9  39491  uzindd  39913  sticksstones1  40030  metakunt12  40064  ofun  40137  fsuppind  40202  mhphf  40208  prjspner1  40384  infdesc  40396  ismrcd1  40436  isnacs3  40448  pellfundglb  40623  jm2.22  40733  jm2.23  40734  isnumbasgrplem1  40842  hbtlem6  40870  rngunsnply  40914  mnringmulrcld  41735  dvgrat  41819  cvgdvgrat  41820  nznngen  41823  uzmptshftfval  41853  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  iccshift  42946  iooshift  42950  liminflbuz2  43246  xlimbr  43258  itgperiod  43412  fourierdlem42  43580  fourierdlem68  43605  fourierdlem93  43630  elprneb  44410  dfatcolem  44634  ichim  44797  ichnfb  44805  prproropf1olem1  44843  prproropf1olem3  44845  rabsubmgmd  45233  2zlidl  45380  lspsslco  45666  isthincd2  46207  fullthinc  46215