Theorem sylan2b 594

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 593	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  598  eupickb  2628  2eu1  2644  2eu1v  2645  elnelne1  3040  elnelne2  3041  morex  3681  psssstr  4062  reuss2  4279  reupick  4282  reximdva0  4308  falseral0  4469  rabsneu  4683  invdisjrab  5082  opabss  5159  triun  5216  triin  5218  poirr  5543  wefrc  5617  xpcan  6129  fnfco  6693  eqfnun  6975  fnressn  7096  fvtp3  7137  fvtp3g  7140  f1mpt  7202  offval  7626  ordsucuniel  7763  onzsl  7786  soex  7861  fiunlem  7884  fiun  7885  f1iun  7886  dfoprab3  7996  poxp  8068  fnwelem  8071  poxp2  8083  suppssr  8135  suppssrg  8136  suppsssn  8141  suppofssd  8143  fprlem2  8241  oeordsuc  8519  oelim2  8520  omsmolem  8582  rexdif1enOLD  9083  ssnnfi  9093  ssfi  9097  ensymfib  9108  domnsymfi  9124  fiint  9235  fiintOLD  9236  unifi  9253  indexfi  9269  iinfi  9326  unwdomg  9495  inf3lem5  9547  rankr1bg  9718  rankr1c  9736  carden2a  9881  dfac8clem  9945  dfac5lem4  10039  dfac5lem4OLD  10041  pwsdompw  10116  cfsuc  10170  cflim2  10176  enfin2i  10234  isf34lem4  10290  axdc4lem  10368  zornn0g  10418  uniimadomf  10458  fpwwe2lem7  10550  fpwwe2lem11  10554  fpwwe2lem12  10555  pwfseqlem1  10571  pwfseqlem5  10576  intgru  10727  addclpi  10805  addnidpi  10814  ltsonq  10882  nqpr  10927  reclem3pr  10962  recexsr  11020  supsrlem  11024  nnnn0addcl  12432  un0addcl  12435  un0mulcl  12436  nn0nndivcl  12474  nn0ge0div  12563  uzind3  12588  uzind4  12825  zsupss  12856  rpnnen1lem2  12896  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  ltsubrp  12949  ltaddrp  12950  xrlttr  13060  qbtwnxr  13120  xltnegi  13136  xaddnemnf  13156  xaddnepnf  13157  xaddcom  13160  xnegdi  13168  xsubge0  13181  xrub  13232  fzne1  13525  fzind2  13706  seqof  13984  expp1  13993  expneg  13994  expcllem  13997  mulexpz  14027  expaddz  14031  expmulz  14033  faclbnd4lem3  14220  faclbnd4  14222  fi1uzind  14432  swrd00  14569  swrd0  14583  cats1un  14645  reuccatpfxs1  14671  cshw0  14718  cshwn  14721  wwlktovfo  14883  shftf  15004  sqrtdiv  15190  leabs  15224  mulcn2  15521  summolem2  15641  fsumrev2  15707  geomulcvg  15801  prodmolem2  15860  zprod  15862  prodsn  15887  prodsnf  15889  fprodle  15921  bpolydiflem  15979  bpoly2  15982  bpoly3  15983  ruclem6  16162  dvdsflip  16246  dvdsfac  16255  gcdcllem1  16428  lcmgcdlem  16535  rpexp1i  16652  hashdvds  16704  hashgcdlem  16717  phisum  16720  iserodd  16765  pcqcl  16786  pcid  16803  ismred  17522  funcpropd  17827  natpropd  17904  odupos  18250  lubun  18439  rabsubmgmd  18596  sgrpidmnd  18631  issubmd  18698  grpinvnzcl  18908  mulgneg  18989  mulgnn0z  18998  symgfixf1  19334  symgsssg  19364  symgfisg  19365  pgpssslw  19511  sylow2alem2  19515  sylow2a  19516  oddvdssubg  19752  gsumzunsnd  19853  gsumunsnfd  19854  gsum2dlem1  19867  gsum2dlem2  19868  gsumcom3  19875  ablfac1eu  19972  pgpfac1lem5  19978  gsumdixp  20222  dvdsrcl2  20269  01eq0ring  20433  isdrngd  20668  isdrngdOLD  20670  cnsubrg  21352  psgnodpm  21513  evlslem4  21999  psdmul  22069  coe1tmmul2  22178  mpomatmul  22349  cpmidpmat  22776  intcld  22943  neiptopnei  23035  ordtrest2lem  23106  lmss  23201  cmpcovf  23294  cncmp  23295  fincmp  23296  cmpsublem  23302  cmpsub  23303  unconn  23332  1stcfb  23348  2ndcsep  23362  refun0  23418  locfincmp  23429  1stckgenlem  23456  ptbasin  23480  ptbasfi  23484  ptunimpt  23498  ptuniconst  23501  dfac14  23521  ptcnp  23525  xkoptsub  23557  xkococnlem  23562  xkoinjcn  23590  qtopcmplem  23610  qtophmeo  23720  fbfinnfr  23744  isufil2  23811  isfcls  23912  xmetrtri  24259  xmetrtri2  24260  blssioo  24699  divcnOLD  24773  divcn  24775  bndth  24873  clmvscom  25006  resscdrg  25274  minveclem3  25345  finiunmbl  25461  opnmbllem  25518  ismbf2d  25557  itg2seq  25659  bddiblnc  25759  ellimc2  25794  limcmpt2  25801  limcres  25803  dvlem  25813  dvidlem  25832  dvrec  25875  dveflem  25899  dvlip  25914  coe1mul3  26020  dvtaylp  26294  leibpilem2  26867  leibpi  26868  wilthlem2  26995  basellem3  27009  dchreq  27185  dchrsum  27196  lgsval3  27242  lgsdir2lem4  27255  2sqlem6  27350  rpvmasumlem  27414  dchrisum0fno1  27438  rpvmasum2  27439  pntrsumbnd2  27494  ostthlem1  27554  nosupno  27631  negsbdaylem  27985  expsp1  28339  colmid  28651  lmiisolem  28759  dfcgra2  28793  axcontlem2  28928  axcontlem7  28933  upgrex  29055  umgredg  29101  umgrpredgv  29103  umgredgne  29108  umgredgnlp  29110  usgredgppr  29159  edgssv2  29161  uspgredg2vlem  29186  usgredg2vlem1  29188  upgrres1  29276  nbuhgr2vtx1edgblem  29314  nbusgrf1o0  29332  hashnbusgrnn0  29339  iscplgredg  29380  uhgrvd00  29498  finsumvtxdg2size  29514  wlkepvtx  29622  wlknewwlksn  29850  wwlksnextfun  29861  wwlksnextsurj  29863  elwwlks2ons3im  29917  wwlks2onsym  29921  clwwlkf  30009  fusgreghash2wspv  30297  numclwwlk5lem  30349  grpoidinvlem3  30468  ablo32  30511  ablomuldiv  30514  ablodivdiv  30515  ablodiv32  30517  nvscom  30591  dipassr  30808  htthlem  30879  hsn0elch  31210  shscli  31279  nmopun  31976  branmfn  32067  mdslj1i  32281  mdslj2i  32282  atss  32308  chcv1  32317  dmdbr5ati  32384  snsssng  32476  ifnebib  32511  fnpreimac  32628  fcnvgreu  32630  isoun  32658  fsuppcurry1  32681  fsuppcurry2  32682  prodpr  32784  prodtp  32785  pmtrprfv2  33043  elrgspnsubrunlem2  33201  nsgmgclem  33361  nsgqusf1olem2  33364  isprmidlc  33397  ssdifidllem  33406  ssdifidlprm  33408  ssmxidllem  33423  qsdrng  33447  1arithufdlem3  33496  ordtrest2NEWlem  33891  esumsplit  34022  esumpad2  34025  esumpcvgval  34047  sigaclcu2  34089  ldgenpisyslem1  34132  volmeas  34200  mbfmco2  34235  omsmeas  34293  oddpwdc  34324  eulerpartlemgvv  34346  ballotlemfc0  34463  ballotlemfcc  34464  prodfzo03  34573  circlemethhgt  34613  bnj1109  34755  bnj1294  34786  bnj545  34864  bnj605  34876  bnj594  34881  bnj934  34904  bnj953  34908  bnj1137  34964  bnj1174  34972  bnj1388  35002  subfacp1lem4  35158  erdszelem7  35172  erdszelem8  35173  erdsze2lem2  35179  resconn  35221  cvmsdisj  35245  cvmscld  35248  satf0op  35352  mclsax  35544  climuzcnv  35646  pocnv  35738  cgrid2  35979  btwncom  35990  btwnswapid2  35994  colinearperm1  36038  colinearperm3  36039  colinearperm2  36040  colinearperm4  36041  lineext  36052  colinbtwnle  36094  broutsideof2  36098  outsideofcom  36104  linecom  36126  linerflx2  36127  lineintmo  36133  fwddifn0  36140  hfext  36159  ntruni  36303  clsint2  36305  neibastop1  36335  weiunlem2  36439  bj-snsetex  36939  relowlssretop  37339  pibt2  37393  fin2solem  37588  lindsadd  37595  matunitlindflem1  37598  poimirlem4  37606  poimirlem25  37627  poimirlem32  37634  opnmbllem0  37638  mblfinlem3  37641  mbfposadd  37649  itg2addnclem3  37655  ftc1anclem6  37680  ftc1anc  37683  ac6gf  37714  heibor1lem  37791  isdrngo2  37940  unichnidl  38013  isfldidl  38050  cnf1dd  38072  membpartlem19  38791  lkrss2N  39150  elpadd0  39791  ltrnu  40103  tendoex  40957  cdlemm10N  41100  dicfnN  41165  dihmeetlem2N  41281  dihlatat  41319  lcfrlem9  41532  uzindd  41953  sticksstones1  42122  ofun  42212  nn0addcom  42438  nn0mulcom  42442  zmulcomlem  42443  fsuppind  42566  prjspner1  42602  infdesc  42619  ismrcd1  42674  isnacs3  42686  pellfundglb  42861  jm2.22  42971  jm2.23  42972  isnumbasgrplem1  43077  hbtlem6  43105  rngunsnply  43145  ordsssucim  43378  mnringmulrcld  44204  dvgrat  44288  cvgdvgrat  44289  nznngen  44292  uzmptshftfval  44322  wfac8prim  44979  rnmptlb  45224  rnmptbddlem  45225  rnmptbd2lem  45229  iccshift  45503  iooshift  45507  liminflbuz2  45800  xlimbr  45812  itgperiod  45966  fourierdlem42  46134  fourierdlem68  46159  fourierdlem93  46184  smfpimne2  46825  elprneb  47017  dfatcolem  47243  modmknepk  47350  ichim  47445  ichnfb  47453  prproropf1olem1  47491  prproropf1olem3  47493  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  2zlidl  48228  lspsslco  48426  isthincd2  49426  fullthinc  49439