Theorem sylan2b 595

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 594	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  599  eupickb  2636  2eu1  2652  2eu1v  2653  elnelne1  3048  elnelne2  3049  morex  3679  psssstr  4063  reuss2  4280  reupick  4283  reximdva0  4309  falseral0OLD  4470  rabsneu  4688  invdisjrab  5087  opabss  5164  triun  5221  triin  5223  poirr  5552  wefrc  5626  xpcan  6142  fnfco  6707  eqfnun  6991  fnressn  7113  fvtp3  7153  fvtp3g  7156  f1mpt  7217  offval  7641  ordsucuniel  7776  onzsl  7798  soex  7873  fiunlem  7896  fiun  7897  f1iun  7898  dfoprab3  8008  poxp  8080  fnwelem  8083  poxp2  8095  suppssr  8147  suppssrg  8148  suppsssn  8153  suppofssd  8155  fprlem2  8253  oeordsuc  8532  oelim2  8533  omsmolem  8595  ssnnfi  9106  ssfi  9109  ensymfib  9120  domnsymfi  9136  fiint  9239  unifi  9256  indexfi  9272  iinfi  9332  unwdomg  9501  inf3lem5  9553  rankr1bg  9727  rankr1c  9745  carden2a  9890  dfac8clem  9954  dfac5lem4  10048  dfac5lem4OLD  10050  pwsdompw  10125  cfsuc  10179  cflim2  10185  enfin2i  10243  isf34lem4  10299  axdc4lem  10377  zornn0g  10427  uniimadomf  10467  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  pwfseqlem1  10581  pwfseqlem5  10586  intgru  10737  addclpi  10815  addnidpi  10824  ltsonq  10892  nqpr  10937  reclem3pr  10972  recexsr  11030  supsrlem  11034  nnnn0addcl  12443  un0addcl  12446  un0mulcl  12447  nn0nndivcl  12485  nn0ge0div  12573  uzind3  12598  uzind4  12831  zsupss  12862  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  ltsubrp  12955  ltaddrp  12956  xrlttr  13066  qbtwnxr  13127  xltnegi  13143  xaddnemnf  13163  xaddnepnf  13164  xaddcom  13167  xnegdi  13175  xsubge0  13188  xrub  13239  fzne1  13532  fzind2  13716  seqof  13994  expp1  14003  expneg  14004  expcllem  14007  mulexpz  14037  expaddz  14041  expmulz  14043  faclbnd4lem3  14230  faclbnd4  14232  fi1uzind  14442  swrd00  14580  swrd0  14594  cats1un  14656  reuccatpfxs1  14682  cshw0  14729  cshwn  14732  wwlktovfo  14893  shftf  15014  sqrtdiv  15200  leabs  15234  mulcn2  15531  summolem2  15651  fsumrev2  15717  geomulcvg  15811  prodmolem2  15870  zprod  15872  prodsn  15897  prodsnf  15899  fprodle  15931  bpolydiflem  15989  bpoly2  15992  bpoly3  15993  ruclem6  16172  dvdsflip  16256  dvdsfac  16265  gcdcllem1  16438  lcmgcdlem  16545  rpexp1i  16662  hashdvds  16714  hashgcdlem  16727  phisum  16730  iserodd  16775  pcqcl  16796  pcid  16813  ismred  17533  funcpropd  17838  natpropd  17915  odupos  18261  lubun  18450  rabsubmgmd  18641  sgrpidmnd  18676  issubmd  18743  grpinvnzcl  18953  mulgneg  19034  mulgnn0z  19043  symgfixf1  19378  symgsssg  19408  symgfisg  19409  pgpssslw  19555  sylow2alem2  19559  sylow2a  19560  oddvdssubg  19796  gsumzunsnd  19897  gsumunsnfd  19898  gsum2dlem1  19911  gsum2dlem2  19912  gsumcom3  19919  ablfac1eu  20016  pgpfac1lem5  20022  gsumdixp  20266  dvdsrcl2  20314  01eq0ring  20475  isdrngd  20710  isdrngdOLD  20712  cnsubrg  21394  psgnodpm  21555  evlslem4  22043  psdmul  22121  coe1tmmul2  22230  mpomatmul  22402  cpmidpmat  22829  intcld  22996  neiptopnei  23088  ordtrest2lem  23159  lmss  23254  cmpcovf  23347  cncmp  23348  fincmp  23349  cmpsublem  23355  cmpsub  23356  unconn  23385  1stcfb  23401  2ndcsep  23415  refun0  23471  locfincmp  23482  1stckgenlem  23509  ptbasin  23533  ptbasfi  23537  ptunimpt  23551  ptuniconst  23554  dfac14  23574  ptcnp  23578  xkoptsub  23610  xkococnlem  23615  xkoinjcn  23643  qtopcmplem  23663  qtophmeo  23773  fbfinnfr  23797  isufil2  23864  isfcls  23965  xmetrtri  24311  xmetrtri2  24312  blssioo  24751  divcnOLD  24825  divcn  24827  bndth  24925  clmvscom  25058  resscdrg  25326  minveclem3  25397  finiunmbl  25513  opnmbllem  25570  ismbf2d  25609  itg2seq  25711  bddiblnc  25811  ellimc2  25846  limcmpt2  25853  limcres  25855  dvlem  25865  dvidlem  25884  dvrec  25927  dveflem  25951  dvlip  25966  coe1mul3  26072  dvtaylp  26346  leibpilem2  26919  leibpi  26920  wilthlem2  27047  basellem3  27061  dchreq  27237  dchrsum  27248  lgsval3  27294  lgsdir2lem4  27307  2sqlem6  27402  rpvmasumlem  27466  dchrisum0fno1  27490  rpvmasum2  27491  pntrsumbnd2  27546  ostthlem1  27606  nosupno  27683  negbdaylem  28064  expsp1  28437  colmid  28772  lmiisolem  28880  dfcgra2  28914  axcontlem2  29050  axcontlem7  29055  upgrex  29177  umgredg  29223  umgrpredgv  29225  umgredgne  29230  umgredgnlp  29232  usgredgppr  29281  edgssv2  29283  uspgredg2vlem  29308  usgredg2vlem1  29310  upgrres1  29398  nbuhgr2vtx1edgblem  29436  nbusgrf1o0  29454  hashnbusgrnn0  29461  iscplgredg  29502  uhgrvd00  29620  finsumvtxdg2size  29636  wlkepvtx  29744  wlknewwlksn  29972  wwlksnextfun  29983  wwlksnextsurj  29985  elwwlks2ons3im  30039  wwlks2onsym  30045  clwwlkf  30134  fusgreghash2wspv  30422  numclwwlk5lem  30474  grpoidinvlem3  30593  ablo32  30636  ablomuldiv  30639  ablodivdiv  30640  ablodiv32  30642  nvscom  30716  dipassr  30933  htthlem  31004  hsn0elch  31335  shscli  31404  nmopun  32101  branmfn  32192  mdslj1i  32406  mdslj2i  32407  atss  32433  chcv1  32442  dmdbr5ati  32509  snsssng  32600  ifnebib  32635  fnpreimac  32759  fcnvgreu  32761  isoun  32791  fsuppcurry1  32813  fsuppcurry2  32814  prodpr  32917  prodtp  32918  pmtrprfv2  33181  elrgspnsubrunlem2  33341  nsgmgclem  33503  nsgqusf1olem2  33506  isprmidlc  33539  ssdifidllem  33548  ssdifidlprm  33550  ssmxidllem  33565  qsdrng  33589  1arithufdlem3  33638  ordtrest2NEWlem  34099  esumsplit  34230  esumpad2  34233  esumpcvgval  34255  sigaclcu2  34297  ldgenpisyslem1  34340  volmeas  34408  mbfmco2  34442  omsmeas  34500  oddpwdc  34531  eulerpartlemgvv  34553  ballotlemfc0  34670  ballotlemfcc  34671  prodfzo03  34780  circlemethhgt  34820  bnj1109  34962  bnj1294  34992  bnj545  35070  bnj605  35082  bnj594  35087  bnj934  35110  bnj953  35114  bnj1137  35170  bnj1174  35178  bnj1388  35208  subfacp1lem4  35396  erdszelem7  35410  erdszelem8  35411  erdsze2lem2  35417  resconn  35459  cvmsdisj  35483  cvmscld  35486  satf0op  35590  mclsax  35782  climuzcnv  35884  pocnv  35976  cgrid2  36216  btwncom  36227  btwnswapid2  36231  colinearperm1  36275  colinearperm3  36276  colinearperm2  36277  colinearperm4  36278  lineext  36289  colinbtwnle  36331  broutsideof2  36335  outsideofcom  36341  linecom  36363  linerflx2  36364  lineintmo  36370  fwddifn0  36377  hfext  36396  ntruni  36540  clsint2  36542  neibastop1  36572  weiunlem  36676  bj-snsetex  37208  relowlssretop  37615  pibt2  37669  fin2solem  37854  lindsadd  37861  matunitlindflem1  37864  poimirlem4  37872  poimirlem25  37893  poimirlem32  37900  opnmbllem0  37904  mblfinlem3  37907  mbfposadd  37915  itg2addnclem3  37921  ftc1anclem6  37946  ftc1anc  37949  ac6gf  37980  heibor1lem  38057  isdrngo2  38206  unichnidl  38279  isfldidl  38316  cnf1dd  38338  membpartlem19  39162  lkrss2N  39542  elpadd0  40182  ltrnu  40494  tendoex  41348  cdlemm10N  41491  dicfnN  41556  dihmeetlem2N  41672  dihlatat  41710  lcfrlem9  41923  uzindd  42344  sticksstones1  42513  ofun  42605  nn0addcom  42829  nn0mulcom  42833  zmulcomlem  42834  fsuppind  42945  prjspner1  42981  infdesc  42998  ismrcd1  43052  isnacs3  43064  pellfundglb  43239  jm2.22  43349  jm2.23  43350  isnumbasgrplem1  43455  hbtlem6  43483  rngunsnply  43523  ordsssucim  43756  mnringmulrcld  44581  dvgrat  44665  cvgdvgrat  44666  nznngen  44669  uzmptshftfval  44699  wfac8prim  45355  rnmptlb  45598  rnmptbddlem  45599  rnmptbd2lem  45603  iccshift  45875  iooshift  45879  liminflbuz2  46170  xlimbr  46182  itgperiod  46336  fourierdlem42  46504  fourierdlem68  46529  fourierdlem93  46554  smfpimne2  47195  elprneb  47386  dfatcolem  47612  modmknepk  47719  ichim  47814  ichnfb  47822  prproropf1olem1  47860  prproropf1olem3  47862  gpgnbgrvtx0  48431  gpgnbgrvtx1  48432  2zlidl  48597  lspsslco  48794  isthincd2  49793  fullthinc  49806