Theorem sylan2b 592

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 591	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

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 395

This theorem is referenced by:  syl2anb  596  eupickb  2629  2eu1  2644  2eu1v  2645  eqtr3OLD  2757  elnelne1  3055  elnelne2  3056  morex  3714  psssstr  4105  reuss2  4314  reupick  4317  reximdva0  4350  falseral0  4518  rabsneu  4732  invdisjrabw  5132  opabss  5211  triun  5279  triin  5281  poirr  5599  wefrc  5669  xpcan  6174  fnfco  6755  eqfnun  7037  fnressn  7157  fvtp3  7199  fvtp3g  7202  f1mpt  7262  offval  7681  ordsucuniel  7814  onzsl  7837  soex  7914  fiunlem  7930  fiun  7931  f1iun  7932  dfoprab3  8042  poxp  8116  fnwelem  8119  poxp2  8131  suppssr  8183  suppssrg  8184  suppsssn  8188  suppofssd  8190  fprlem2  8288  oeordsuc  8596  oelim2  8597  omsmolem  8658  rexdif1enOLD  9161  ssnnfi  9171  ssnnfiOLD  9172  ssfi  9175  ensymfib  9189  domnsymfi  9205  fiint  9326  unifi  9343  indexfi  9362  iinfi  9414  unwdomg  9581  inf3lem5  9629  rankr1bg  9800  rankr1c  9818  carden2a  9963  dfac8clem  10029  dfac5lem4  10123  pwsdompw  10201  cfsuc  10254  cflim2  10260  enfin2i  10318  isf34lem4  10374  axdc4lem  10452  zornn0g  10502  uniimadomf  10542  fpwwe2lem7  10634  fpwwe2lem11  10638  fpwwe2lem12  10639  pwfseqlem1  10655  pwfseqlem5  10660  intgru  10811  addclpi  10889  addnidpi  10898  ltsonq  10966  nqpr  11011  reclem3pr  11046  recexsr  11104  supsrlem  11108  nnnn0addcl  12506  un0addcl  12509  un0mulcl  12510  nn0nndivcl  12547  nn0ge0div  12635  uzind3  12660  uzind4  12894  zsupss  12925  rpnnen1lem2  12965  rpnnen1lem1  12966  rpnnen1lem3  12967  rpnnen1lem5  12969  ltsubrp  13014  ltaddrp  13015  xrlttr  13123  qbtwnxr  13183  xltnegi  13199  xaddnemnf  13219  xaddnepnf  13220  xaddcom  13223  xnegdi  13231  xsubge0  13244  xrub  13295  fzind2  13754  seqof  14029  expp1  14038  expneg  14039  expcllem  14042  mulexpz  14072  expaddz  14076  expmulz  14078  faclbnd4lem3  14259  faclbnd4  14261  fi1uzind  14462  swrd00  14598  swrd0  14612  cats1un  14675  reuccatpfxs1  14701  cshw0  14748  cshwn  14751  wwlktovfo  14913  shftf  15030  sqrtdiv  15216  leabs  15250  mulcn2  15544  summolem2  15666  fsumrev2  15732  geomulcvg  15826  prodmolem2  15883  zprod  15885  prodsn  15910  prodsnf  15912  fprodle  15944  bpolydiflem  16002  bpoly2  16005  bpoly3  16006  ruclem6  16182  dvdsflip  16264  dvdsfac  16273  gcdcllem1  16444  lcmgcdlem  16547  rpexp1i  16664  hashdvds  16712  hashgcdlem  16725  phisum  16727  iserodd  16772  pcqcl  16793  pcid  16810  ismred  17550  funcpropd  17855  natpropd  17933  odupos  18285  lubun  18472  rabsubmgmd  18629  sgrpidmnd  18664  issubmd  18723  grpinvnzcl  18931  mulgneg  19008  mulgnn0z  19017  symgfixf1  19346  symgsssg  19376  symgfisg  19377  pgpssslw  19523  sylow2alem2  19527  sylow2a  19528  oddvdssubg  19764  gsumzunsnd  19865  gsumunsnfd  19866  gsum2dlem1  19879  gsum2dlem2  19880  gsumcom3  19887  ablfac1eu  19984  pgpfac1lem5  19990  gsumdixp  20207  dvdsrcl2  20257  01eq0ring  20419  isdrngd  20533  isdrngdOLD  20535  cnsubrg  21205  psgnodpm  21360  evlslem4  21856  coe1tmmul2  22018  mpomatmul  22168  cpmidpmat  22595  intcld  22764  neiptopnei  22856  ordtrest2lem  22927  lmss  23022  cmpcovf  23115  cncmp  23116  fincmp  23117  cmpsublem  23123  cmpsub  23124  unconn  23153  1stcfb  23169  2ndcsep  23183  refun0  23239  locfincmp  23250  1stckgenlem  23277  ptbasin  23301  ptbasfi  23305  ptunimpt  23319  ptuniconst  23322  dfac14  23342  ptcnp  23346  xkoptsub  23378  xkococnlem  23383  xkoinjcn  23411  qtopcmplem  23431  qtophmeo  23541  fbfinnfr  23565  isufil2  23632  isfcls  23733  xmetrtri  24081  xmetrtri2  24082  blssioo  24531  divcnOLD  24604  divcn  24606  bndth  24704  clmvscom  24837  resscdrg  25106  minveclem3  25177  finiunmbl  25293  opnmbllem  25350  ismbf2d  25389  itg2seq  25492  bddiblnc  25591  ellimc2  25626  limcmpt2  25633  limcres  25635  dvlem  25645  dvidlem  25664  dvrec  25707  dveflem  25731  dvlip  25745  coe1mul3  25852  dvtaylp  26118  leibpilem2  26682  leibpi  26683  wilthlem2  26809  basellem3  26823  dchreq  26997  dchrsum  27008  lgsval3  27054  lgsdir2lem4  27067  2sqlem6  27162  rpvmasumlem  27226  dchrisum0fno1  27250  rpvmasum2  27251  pntrsumbnd2  27306  ostthlem1  27366  nosupno  27442  negsbdaylem  27769  colmid  28206  lmiisolem  28314  dfcgra2  28348  axcontlem2  28490  axcontlem7  28495  upgrex  28619  umgredg  28665  umgrpredgv  28667  umgredgne  28672  umgredgnlp  28674  usgredgppr  28720  edgssv2  28722  uspgredg2vlem  28747  usgredg2vlem1  28749  upgrres1  28837  nbuhgr2vtx1edgblem  28875  nbusgrf1o0  28893  hashnbusgrnn0  28900  iscplgredg  28941  uhgrvd00  29058  finsumvtxdg2size  29074  wlkepvtx  29184  wlknewwlksn  29408  wwlksnextfun  29419  wwlksnextsurj  29421  elwwlks2ons3im  29475  wwlks2onsym  29479  clwwlkf  29567  fusgreghash2wspv  29855  numclwwlk5lem  29907  grpoidinvlem3  30026  ablo32  30069  ablomuldiv  30072  ablodivdiv  30073  ablodiv32  30075  nvscom  30149  dipassr  30366  htthlem  30437  hsn0elch  30768  shscli  30837  nmopun  31534  branmfn  31625  mdslj1i  31839  mdslj2i  31840  atss  31866  chcv1  31875  dmdbr5ati  31942  snsssng  32019  ifnebib  32048  fnpreimac  32163  fcnvgreu  32165  isoun  32190  fsuppcurry1  32217  fsuppcurry2  32218  fzne1  32266  prodpr  32299  prodtp  32300  pmtrprfv2  32519  nsgmgclem  32796  nsgqusf1olem2  32799  isprmidlc  32840  ssmxidllem  32863  qsdrng  32885  ordtrest2NEWlem  33200  esumsplit  33349  esumpad2  33352  esumpcvgval  33374  sigaclcu2  33416  ldgenpisyslem1  33459  volmeas  33527  mbfmco2  33562  omsmeas  33620  oddpwdc  33651  eulerpartlemgvv  33673  ballotlemfc0  33789  ballotlemfcc  33790  prodfzo03  33913  circlemethhgt  33953  bnj1109  34095  bnj1294  34126  bnj545  34204  bnj605  34216  bnj594  34221  bnj934  34244  bnj953  34248  bnj1137  34304  bnj1174  34312  bnj1388  34342  subfacp1lem4  34472  erdszelem7  34486  erdszelem8  34487  erdsze2lem2  34493  resconn  34535  cvmsdisj  34559  cvmscld  34562  satf0op  34666  mclsax  34858  climuzcnv  34954  pocnv  35037  cgrid2  35279  btwncom  35290  btwnswapid2  35294  colinearperm1  35338  colinearperm3  35339  colinearperm2  35340  colinearperm4  35341  lineext  35352  colinbtwnle  35394  broutsideof2  35398  outsideofcom  35404  linecom  35426  linerflx2  35427  lineintmo  35433  fwddifn0  35440  hfext  35459  ntruni  35515  clsint2  35517  neibastop1  35547  bj-snsetex  36147  relowlssretop  36547  pibt2  36601  fin2solem  36777  lindsadd  36784  matunitlindflem1  36787  poimirlem4  36795  poimirlem25  36816  poimirlem32  36823  opnmbllem0  36827  mblfinlem3  36830  mbfposadd  36838  itg2addnclem3  36844  ftc1anclem6  36869  ftc1anc  36872  ac6gf  36903  heibor1lem  36980  isdrngo2  37129  unichnidl  37202  isfldidl  37239  cnf1dd  37261  membpartlem19  37984  lkrss2N  38342  elpadd0  38983  ltrnu  39295  tendoex  40149  cdlemm10N  40292  dicfnN  40357  dihmeetlem2N  40473  dihlatat  40511  lcfrlem9  40724  uzindd  41148  sticksstones1  41268  metakunt12  41302  ofun  41364  fsuppind  41464  nn0addcom  41625  nn0mulcom  41629  zmulcomlem  41630  prjspner1  41670  infdesc  41687  ismrcd1  41738  isnacs3  41750  pellfundglb  41925  jm2.22  42036  jm2.23  42037  isnumbasgrplem1  42145  hbtlem6  42173  rngunsnply  42217  ordsssucim  42455  mnringmulrcld  43289  dvgrat  43373  cvgdvgrat  43374  nznngen  43377  uzmptshftfval  43407  rnmptlb  44245  rnmptbddlem  44246  rnmptbd2lem  44250  iccshift  44529  iooshift  44533  liminflbuz2  44829  xlimbr  44841  itgperiod  44995  fourierdlem42  45163  fourierdlem68  45188  fourierdlem93  45213  smfpimne2  45854  elprneb  46037  dfatcolem  46261  ichim  46423  ichnfb  46431  prproropf1olem1  46469  prproropf1olem3  46471  2zlidl  46920  lspsslco  47205  isthincd2  47745  fullthinc  47753