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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  syl2anb  597  eupickb  2638  2eu1  2654  2eu1v  2655  eqtr3OLD  2767  elnelne1  3063  elnelne2  3064  morex  3741  psssstr  4132  reuss2  4345  reupick  4348  reximdva0  4378  falseral0  4539  rabsneu  4754  invdisjrab  5153  opabss  5230  triun  5298  triin  5300  poirr  5620  wefrc  5694  xpcan  6207  fnfco  6786  eqfnun  7070  fnressn  7192  fvtp3  7234  fvtp3g  7237  f1mpt  7298  offval  7723  ordsucuniel  7860  onzsl  7883  soex  7961  fiunlem  7982  fiun  7983  f1iun  7984  dfoprab3  8095  poxp  8169  fnwelem  8172  poxp2  8184  suppssr  8236  suppssrg  8237  suppsssn  8242  suppofssd  8244  fprlem2  8342  oeordsuc  8650  oelim2  8651  omsmolem  8713  rexdif1enOLD  9225  ssnnfi  9235  ssnnfiOLD  9236  ssfi  9240  ensymfib  9250  domnsymfi  9266  fiint  9394  fiintOLD  9395  unifi  9412  indexfi  9430  iinfi  9486  unwdomg  9653  inf3lem5  9701  rankr1bg  9872  rankr1c  9890  carden2a  10035  dfac8clem  10101  dfac5lem4  10195  dfac5lem4OLD  10197  pwsdompw  10272  cfsuc  10326  cflim2  10332  enfin2i  10390  isf34lem4  10446  axdc4lem  10524  zornn0g  10574  uniimadomf  10614  fpwwe2lem7  10706  fpwwe2lem11  10710  fpwwe2lem12  10711  pwfseqlem1  10727  pwfseqlem5  10732  intgru  10883  addclpi  10961  addnidpi  10970  ltsonq  11038  nqpr  11083  reclem3pr  11118  recexsr  11176  supsrlem  11180  nnnn0addcl  12583  un0addcl  12586  un0mulcl  12587  nn0nndivcl  12624  nn0ge0div  12712  uzind3  12737  uzind4  12971  zsupss  13002  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  ltsubrp  13093  ltaddrp  13094  xrlttr  13202  qbtwnxr  13262  xltnegi  13278  xaddnemnf  13298  xaddnepnf  13299  xaddcom  13302  xnegdi  13310  xsubge0  13323  xrub  13374  fzind2  13835  seqof  14110  expp1  14119  expneg  14120  expcllem  14123  mulexpz  14153  expaddz  14157  expmulz  14159  faclbnd4lem3  14344  faclbnd4  14346  fi1uzind  14556  swrd00  14692  swrd0  14706  cats1un  14769  reuccatpfxs1  14795  cshw0  14842  cshwn  14845  wwlktovfo  15007  shftf  15128  sqrtdiv  15314  leabs  15348  mulcn2  15642  summolem2  15764  fsumrev2  15830  geomulcvg  15924  prodmolem2  15983  zprod  15985  prodsn  16010  prodsnf  16012  fprodle  16044  bpolydiflem  16102  bpoly2  16105  bpoly3  16106  ruclem6  16283  dvdsflip  16365  dvdsfac  16374  gcdcllem1  16545  lcmgcdlem  16653  rpexp1i  16770  hashdvds  16822  hashgcdlem  16835  phisum  16837  iserodd  16882  pcqcl  16903  pcid  16920  ismred  17660  funcpropd  17967  natpropd  18046  odupos  18398  lubun  18585  rabsubmgmd  18742  sgrpidmnd  18777  issubmd  18841  grpinvnzcl  19051  mulgneg  19132  mulgnn0z  19141  symgfixf1  19479  symgsssg  19509  symgfisg  19510  pgpssslw  19656  sylow2alem2  19660  sylow2a  19661  oddvdssubg  19897  gsumzunsnd  19998  gsumunsnfd  19999  gsum2dlem1  20012  gsum2dlem2  20013  gsumcom3  20020  ablfac1eu  20117  pgpfac1lem5  20123  gsumdixp  20342  dvdsrcl2  20392  01eq0ring  20556  isdrngd  20787  isdrngdOLD  20789  cnsubrg  21468  psgnodpm  21629  evlslem4  22123  psdmul  22193  coe1tmmul2  22300  mpomatmul  22473  cpmidpmat  22900  intcld  23069  neiptopnei  23161  ordtrest2lem  23232  lmss  23327  cmpcovf  23420  cncmp  23421  fincmp  23422  cmpsublem  23428  cmpsub  23429  unconn  23458  1stcfb  23474  2ndcsep  23488  refun0  23544  locfincmp  23555  1stckgenlem  23582  ptbasin  23606  ptbasfi  23610  ptunimpt  23624  ptuniconst  23627  dfac14  23647  ptcnp  23651  xkoptsub  23683  xkococnlem  23688  xkoinjcn  23716  qtopcmplem  23736  qtophmeo  23846  fbfinnfr  23870  isufil2  23937  isfcls  24038  xmetrtri  24386  xmetrtri2  24387  blssioo  24836  divcnOLD  24909  divcn  24911  bndth  25009  clmvscom  25142  resscdrg  25411  minveclem3  25482  finiunmbl  25598  opnmbllem  25655  ismbf2d  25694  itg2seq  25797  bddiblnc  25897  ellimc2  25932  limcmpt2  25939  limcres  25941  dvlem  25951  dvidlem  25970  dvrec  26013  dveflem  26037  dvlip  26052  coe1mul3  26158  dvtaylp  26430  leibpilem2  27002  leibpi  27003  wilthlem2  27130  basellem3  27144  dchreq  27320  dchrsum  27331  lgsval3  27377  lgsdir2lem4  27390  2sqlem6  27485  rpvmasumlem  27549  dchrisum0fno1  27573  rpvmasum2  27574  pntrsumbnd2  27629  ostthlem1  27689  nosupno  27766  negsbdaylem  28106  expsp1  28430  colmid  28714  lmiisolem  28822  dfcgra2  28856  axcontlem2  28998  axcontlem7  29003  upgrex  29127  umgredg  29173  umgrpredgv  29175  umgredgne  29180  umgredgnlp  29182  usgredgppr  29231  edgssv2  29233  uspgredg2vlem  29258  usgredg2vlem1  29260  upgrres1  29348  nbuhgr2vtx1edgblem  29386  nbusgrf1o0  29404  hashnbusgrnn0  29411  iscplgredg  29452  uhgrvd00  29570  finsumvtxdg2size  29586  wlkepvtx  29696  wlknewwlksn  29920  wwlksnextfun  29931  wwlksnextsurj  29933  elwwlks2ons3im  29987  wwlks2onsym  29991  clwwlkf  30079  fusgreghash2wspv  30367  numclwwlk5lem  30419  grpoidinvlem3  30538  ablo32  30581  ablomuldiv  30584  ablodivdiv  30585  ablodiv32  30587  nvscom  30661  dipassr  30878  htthlem  30949  hsn0elch  31280  shscli  31349  nmopun  32046  branmfn  32137  mdslj1i  32351  mdslj2i  32352  atss  32378  chcv1  32387  dmdbr5ati  32454  snsssng  32543  ifnebib  32572  fnpreimac  32689  fcnvgreu  32691  isoun  32713  fsuppcurry1  32739  fsuppcurry2  32740  fzne1  32793  prodpr  32830  prodtp  32831  pmtrprfv2  33081  nsgmgclem  33404  nsgqusf1olem2  33407  isprmidlc  33440  ssdifidllem  33449  ssdifidlprm  33451  ssmxidllem  33466  qsdrng  33490  1arithufdlem3  33539  ordtrest2NEWlem  33868  esumsplit  34017  esumpad2  34020  esumpcvgval  34042  sigaclcu2  34084  ldgenpisyslem1  34127  volmeas  34195  mbfmco2  34230  omsmeas  34288  oddpwdc  34319  eulerpartlemgvv  34341  ballotlemfc0  34457  ballotlemfcc  34458  prodfzo03  34580  circlemethhgt  34620  bnj1109  34762  bnj1294  34793  bnj545  34871  bnj605  34883  bnj594  34888  bnj934  34911  bnj953  34915  bnj1137  34971  bnj1174  34979  bnj1388  35009  subfacp1lem4  35151  erdszelem7  35165  erdszelem8  35166  erdsze2lem2  35172  resconn  35214  cvmsdisj  35238  cvmscld  35241  satf0op  35345  mclsax  35537  climuzcnv  35639  pocnv  35725  cgrid2  35967  btwncom  35978  btwnswapid2  35982  colinearperm1  36026  colinearperm3  36027  colinearperm2  36028  colinearperm4  36029  lineext  36040  colinbtwnle  36082  broutsideof2  36086  outsideofcom  36092  linecom  36114  linerflx2  36115  lineintmo  36121  fwddifn0  36128  hfext  36147  ntruni  36293  clsint2  36295  neibastop1  36325  weiunlem2  36429  bj-snsetex  36929  relowlssretop  37329  pibt2  37383  fin2solem  37566  lindsadd  37573  matunitlindflem1  37576  poimirlem4  37584  poimirlem25  37605  poimirlem32  37612  opnmbllem0  37616  mblfinlem3  37619  mbfposadd  37627  itg2addnclem3  37633  ftc1anclem6  37658  ftc1anc  37661  ac6gf  37692  heibor1lem  37769  isdrngo2  37918  unichnidl  37991  isfldidl  38028  cnf1dd  38050  membpartlem19  38767  lkrss2N  39125  elpadd0  39766  ltrnu  40078  tendoex  40932  cdlemm10N  41075  dicfnN  41140  dihmeetlem2N  41256  dihlatat  41294  lcfrlem9  41507  uzindd  41933  sticksstones1  42103  metakunt12  42173  ofun  42231  nn0addcom  42426  nn0mulcom  42430  zmulcomlem  42431  fsuppind  42545  prjspner1  42581  infdesc  42598  ismrcd1  42654  isnacs3  42666  pellfundglb  42841  jm2.22  42952  jm2.23  42953  isnumbasgrplem1  43058  hbtlem6  43086  rngunsnply  43130  ordsssucim  43364  mnringmulrcld  44197  dvgrat  44281  cvgdvgrat  44282  nznngen  44285  uzmptshftfval  44315  rnmptlb  45152  rnmptbddlem  45153  rnmptbd2lem  45157  iccshift  45436  iooshift  45440  liminflbuz2  45736  xlimbr  45748  itgperiod  45902  fourierdlem42  46070  fourierdlem68  46095  fourierdlem93  46120  smfpimne2  46761  elprneb  46944  dfatcolem  47170  ichim  47331  ichnfb  47339  prproropf1olem1  47377  prproropf1olem3  47379  2zlidl  47963  lspsslco  48166  isthincd2  48705  fullthinc  48713