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  2635  2eu1  2651  2eu1v  2652  elnelne1  3047  elnelne2  3048  morex  3665  psssstr  4049  reuss2  4266  reupick  4269  reximdva0  4295  falseral0OLD  4455  rabsneu  4673  invdisjrab  5072  opabss  5149  triun  5207  triin  5209  poirr  5551  wefrc  5625  xpcan  6140  fnfco  6705  eqfnun  6989  fnressn  7112  fvtp3  7152  fvtp3g  7155  f1mpt  7216  offval  7640  ordsucuniel  7775  onzsl  7797  soex  7872  fiunlem  7895  fiun  7896  f1iun  7897  dfoprab3  8007  poxp  8078  fnwelem  8081  poxp2  8093  suppssr  8145  suppssrg  8146  suppsssn  8151  suppofssd  8153  fprlem2  8251  oeordsuc  8530  oelim2  8531  omsmolem  8593  ssnnfi  9104  ssfi  9107  ensymfib  9118  domnsymfi  9134  fiint  9237  unifi  9254  indexfi  9270  iinfi  9330  unwdomg  9499  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  12467  un0addcl  12470  un0mulcl  12471  nn0nndivcl  12509  nn0ge0div  12598  uzind3  12623  uzind4  12856  zsupss  12887  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  ltsubrp  12980  ltaddrp  12981  xrlttr  13091  qbtwnxr  13152  xltnegi  13168  xaddnemnf  13188  xaddnepnf  13189  xaddcom  13192  xnegdi  13200  xsubge0  13213  xrub  13264  fzne1  13558  fzind2  13743  seqof  14021  expp1  14030  expneg  14031  expcllem  14034  mulexpz  14064  expaddz  14068  expmulz  14070  faclbnd4lem3  14257  faclbnd4  14259  fi1uzind  14469  swrd00  14607  swrd0  14621  cats1un  14683  reuccatpfxs1  14709  cshw0  14756  cshwn  14759  wwlktovfo  14920  shftf  15041  sqrtdiv  15227  leabs  15261  mulcn2  15558  summolem2  15678  fsumrev2  15744  geomulcvg  15841  prodmolem2  15900  zprod  15902  prodsn  15927  prodsnf  15929  fprodle  15961  bpolydiflem  16019  bpoly2  16022  bpoly3  16023  ruclem6  16202  dvdsflip  16286  dvdsfac  16295  gcdcllem1  16468  lcmgcdlem  16575  rpexp1i  16693  hashdvds  16745  hashgcdlem  16758  phisum  16761  iserodd  16806  pcqcl  16827  pcid  16844  ismred  17564  funcpropd  17869  natpropd  17946  odupos  18292  lubun  18481  rabsubmgmd  18672  sgrpidmnd  18707  issubmd  18774  grpinvnzcl  18987  mulgneg  19068  mulgnn0z  19077  symgfixf1  19412  symgsssg  19442  symgfisg  19443  pgpssslw  19589  sylow2alem2  19593  sylow2a  19594  oddvdssubg  19830  gsumzunsnd  19931  gsumunsnfd  19932  gsum2dlem1  19945  gsum2dlem2  19946  gsumcom3  19953  ablfac1eu  20050  pgpfac1lem5  20056  gsumdixp  20298  dvdsrcl2  20346  01eq0ring  20507  isdrngd  20742  isdrngdOLD  20744  cnsubrg  21407  psgnodpm  21568  evlslem4  22054  psdmul  22132  coe1tmmul2  22241  mpomatmul  22411  cpmidpmat  22838  intcld  23005  neiptopnei  23097  ordtrest2lem  23168  lmss  23263  cmpcovf  23356  cncmp  23357  fincmp  23358  cmpsublem  23364  cmpsub  23365  unconn  23394  1stcfb  23410  2ndcsep  23424  refun0  23480  locfincmp  23491  1stckgenlem  23518  ptbasin  23542  ptbasfi  23546  ptunimpt  23560  ptuniconst  23563  dfac14  23583  ptcnp  23587  xkoptsub  23619  xkococnlem  23624  xkoinjcn  23652  qtopcmplem  23672  qtophmeo  23782  fbfinnfr  23806  isufil2  23873  isfcls  23974  xmetrtri  24320  xmetrtri2  24321  blssioo  24760  divcn  24835  bndth  24925  clmvscom  25057  resscdrg  25325  minveclem3  25396  finiunmbl  25511  opnmbllem  25568  ismbf2d  25607  itg2seq  25709  bddiblnc  25809  ellimc2  25844  limcmpt2  25851  limcres  25853  dvlem  25863  dvidlem  25882  dvrec  25922  dveflem  25946  dvlip  25960  coe1mul3  26064  dvtaylp  26335  leibpilem2  26905  leibpi  26906  wilthlem2  27032  basellem3  27046  dchreq  27221  dchrsum  27232  lgsval3  27278  lgsdir2lem4  27291  2sqlem6  27386  rpvmasumlem  27450  dchrisum0fno1  27474  rpvmasum2  27475  pntrsumbnd2  27530  ostthlem1  27590  nosupno  27667  negbdaylem  28048  expsp1  28421  colmid  28756  lmiisolem  28864  dfcgra2  28898  axcontlem2  29034  axcontlem7  29039  upgrex  29161  umgredg  29207  umgrpredgv  29209  umgredgne  29214  umgredgnlp  29216  usgredgppr  29265  edgssv2  29267  uspgredg2vlem  29292  usgredg2vlem1  29294  upgrres1  29382  nbuhgr2vtx1edgblem  29420  nbusgrf1o0  29438  hashnbusgrnn0  29445  iscplgredg  29486  uhgrvd00  29603  finsumvtxdg2size  29619  wlkepvtx  29727  wlknewwlksn  29955  wwlksnextfun  29966  wwlksnextsurj  29968  elwwlks2ons3im  30022  wwlks2onsym  30028  clwwlkf  30117  fusgreghash2wspv  30405  numclwwlk5lem  30457  grpoidinvlem3  30577  ablo32  30620  ablomuldiv  30623  ablodivdiv  30624  ablodiv32  30626  nvscom  30700  dipassr  30917  htthlem  30988  hsn0elch  31319  shscli  31388  nmopun  32085  branmfn  32176  mdslj1i  32390  mdslj2i  32391  atss  32417  chcv1  32426  dmdbr5ati  32493  snsssng  32584  ifnebib  32619  fnpreimac  32743  fcnvgreu  32745  isoun  32775  fsuppcurry1  32797  fsuppcurry2  32798  prodpr  32899  prodtp  32900  pmtrprfv2  33149  elrgspnsubrunlem2  33309  nsgmgclem  33471  nsgqusf1olem2  33474  isprmidlc  33507  ssdifidllem  33516  ssdifidlprm  33518  ssmxidllem  33533  qsdrng  33557  1arithufdlem3  33606  ordtrest2NEWlem  34066  esumsplit  34197  esumpad2  34200  esumpcvgval  34222  sigaclcu2  34264  ldgenpisyslem1  34307  volmeas  34375  mbfmco2  34409  omsmeas  34467  oddpwdc  34498  eulerpartlemgvv  34520  ballotlemfc0  34637  ballotlemfcc  34638  prodfzo03  34747  circlemethhgt  34787  bnj1109  34929  bnj1294  34959  bnj545  35037  bnj605  35049  bnj594  35054  bnj934  35077  bnj953  35081  bnj1137  35137  bnj1174  35145  bnj1388  35175  subfacp1lem4  35365  erdszelem7  35379  erdszelem8  35380  erdsze2lem2  35386  resconn  35428  cvmsdisj  35452  cvmscld  35455  satf0op  35559  mclsax  35751  climuzcnv  35853  pocnv  35945  cgrid2  36185  btwncom  36196  btwnswapid2  36200  colinearperm1  36244  colinearperm3  36245  colinearperm2  36246  colinearperm4  36247  lineext  36258  colinbtwnle  36300  broutsideof2  36304  outsideofcom  36310  linecom  36332  linerflx2  36333  lineintmo  36339  fwddifn0  36346  hfext  36365  ntruni  36509  clsint2  36511  neibastop1  36541  weiunlem  36645  bj-snsetex  37270  relowlssretop  37679  pibt2  37733  fin2solem  37927  lindsadd  37934  matunitlindflem1  37937  poimirlem4  37945  poimirlem25  37966  poimirlem32  37973  opnmbllem0  37977  mblfinlem3  37980  mbfposadd  37988  itg2addnclem3  37994  ftc1anclem6  38019  ftc1anc  38022  ac6gf  38053  heibor1lem  38130  isdrngo2  38279  unichnidl  38352  isfldidl  38389  cnf1dd  38411  membpartlem19  39235  lkrss2N  39615  elpadd0  40255  ltrnu  40567  tendoex  41421  cdlemm10N  41564  dicfnN  41629  dihmeetlem2N  41745  dihlatat  41783  lcfrlem9  41996  uzindd  42417  sticksstones1  42585  ofun  42677  nn0addcom  42907  nn0mulcom  42911  zmulcomlem  42912  fsuppind  43023  prjspner1  43059  infdesc  43076  ismrcd1  43130  isnacs3  43142  pellfundglb  43313  jm2.22  43423  jm2.23  43424  isnumbasgrplem1  43529  hbtlem6  43557  rngunsnply  43597  ordsssucim  43830  mnringmulrcld  44655  dvgrat  44739  cvgdvgrat  44740  nznngen  44743  uzmptshftfval  44773  wfac8prim  45429  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  iccshift  45948  iooshift  45952  liminflbuz2  46243  xlimbr  46255  itgperiod  46409  fourierdlem42  46577  fourierdlem68  46602  fourierdlem93  46627  smfpimne2  47268  elprneb  47477  dfatcolem  47703  modmknepk  47816  ichim  47917  ichnfb  47925  prproropf1olem1  47963  prproropf1olem3  47965  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  2zlidl  48716  lspsslco  48913  isthincd2  49912  fullthinc  49925