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  3666  psssstr  4050  reuss2  4267  reupick  4270  reximdva0  4296  falseral0OLD  4456  rabsneu  4674  invdisjrab  5073  opabss  5150  triun  5207  triin  5209  poirr  5544  wefrc  5618  xpcan  6134  fnfco  6699  eqfnun  6983  fnressn  7105  fvtp3  7145  fvtp3g  7148  f1mpt  7209  offval  7633  ordsucuniel  7768  onzsl  7790  soex  7865  fiunlem  7888  fiun  7889  f1iun  7890  dfoprab3  8000  poxp  8071  fnwelem  8074  poxp2  8086  suppssr  8138  suppssrg  8139  suppsssn  8144  suppofssd  8146  fprlem2  8244  oeordsuc  8523  oelim2  8524  omsmolem  8586  ssnnfi  9097  ssfi  9100  ensymfib  9111  domnsymfi  9127  fiint  9230  unifi  9247  indexfi  9263  iinfi  9323  unwdomg  9492  inf3lem5  9544  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  10551  fpwwe2lem11  10555  fpwwe2lem12  10556  pwfseqlem1  10572  pwfseqlem5  10577  intgru  10728  addclpi  10806  addnidpi  10815  ltsonq  10883  nqpr  10928  reclem3pr  10963  recexsr  11021  supsrlem  11025  nnnn0addcl  12458  un0addcl  12461  un0mulcl  12462  nn0nndivcl  12500  nn0ge0div  12589  uzind3  12614  uzind4  12847  zsupss  12878  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  ltsubrp  12971  ltaddrp  12972  xrlttr  13082  qbtwnxr  13143  xltnegi  13159  xaddnemnf  13179  xaddnepnf  13180  xaddcom  13183  xnegdi  13191  xsubge0  13204  xrub  13255  fzne1  13549  fzind2  13734  seqof  14012  expp1  14021  expneg  14022  expcllem  14025  mulexpz  14055  expaddz  14059  expmulz  14061  faclbnd4lem3  14248  faclbnd4  14250  fi1uzind  14460  swrd00  14598  swrd0  14612  cats1un  14674  reuccatpfxs1  14700  cshw0  14747  cshwn  14750  wwlktovfo  14911  shftf  15032  sqrtdiv  15218  leabs  15252  mulcn2  15549  summolem2  15669  fsumrev2  15735  geomulcvg  15832  prodmolem2  15891  zprod  15893  prodsn  15918  prodsnf  15920  fprodle  15952  bpolydiflem  16010  bpoly2  16013  bpoly3  16014  ruclem6  16193  dvdsflip  16277  dvdsfac  16286  gcdcllem1  16459  lcmgcdlem  16566  rpexp1i  16684  hashdvds  16736  hashgcdlem  16749  phisum  16752  iserodd  16797  pcqcl  16818  pcid  16835  ismred  17555  funcpropd  17860  natpropd  17937  odupos  18283  lubun  18472  rabsubmgmd  18663  sgrpidmnd  18698  issubmd  18765  grpinvnzcl  18978  mulgneg  19059  mulgnn0z  19068  symgfixf1  19403  symgsssg  19433  symgfisg  19434  pgpssslw  19580  sylow2alem2  19584  sylow2a  19585  oddvdssubg  19821  gsumzunsnd  19922  gsumunsnfd  19923  gsum2dlem1  19936  gsum2dlem2  19937  gsumcom3  19944  ablfac1eu  20041  pgpfac1lem5  20047  gsumdixp  20289  dvdsrcl2  20337  01eq0ring  20498  isdrngd  20733  isdrngdOLD  20735  cnsubrg  21417  psgnodpm  21578  evlslem4  22064  psdmul  22142  coe1tmmul2  22251  mpomatmul  22421  cpmidpmat  22848  intcld  23015  neiptopnei  23107  ordtrest2lem  23178  lmss  23273  cmpcovf  23366  cncmp  23367  fincmp  23368  cmpsublem  23374  cmpsub  23375  unconn  23404  1stcfb  23420  2ndcsep  23434  refun0  23490  locfincmp  23501  1stckgenlem  23528  ptbasin  23552  ptbasfi  23556  ptunimpt  23570  ptuniconst  23573  dfac14  23593  ptcnp  23597  xkoptsub  23629  xkococnlem  23634  xkoinjcn  23662  qtopcmplem  23682  qtophmeo  23792  fbfinnfr  23816  isufil2  23883  isfcls  23984  xmetrtri  24330  xmetrtri2  24331  blssioo  24770  divcn  24845  bndth  24935  clmvscom  25067  resscdrg  25335  minveclem3  25406  finiunmbl  25521  opnmbllem  25578  ismbf2d  25617  itg2seq  25719  bddiblnc  25819  ellimc2  25854  limcmpt2  25861  limcres  25863  dvlem  25873  dvidlem  25892  dvrec  25932  dveflem  25956  dvlip  25970  coe1mul3  26074  dvtaylp  26347  leibpilem2  26918  leibpi  26919  wilthlem2  27046  basellem3  27060  dchreq  27235  dchrsum  27246  lgsval3  27292  lgsdir2lem4  27305  2sqlem6  27400  rpvmasumlem  27464  dchrisum0fno1  27488  rpvmasum2  27489  pntrsumbnd2  27544  ostthlem1  27604  nosupno  27681  negbdaylem  28062  expsp1  28435  colmid  28770  lmiisolem  28878  dfcgra2  28912  axcontlem2  29048  axcontlem7  29053  upgrex  29175  umgredg  29221  umgrpredgv  29223  umgredgne  29228  umgredgnlp  29230  usgredgppr  29279  edgssv2  29281  uspgredg2vlem  29306  usgredg2vlem1  29308  upgrres1  29396  nbuhgr2vtx1edgblem  29434  nbusgrf1o0  29452  hashnbusgrnn0  29459  iscplgredg  29500  uhgrvd00  29618  finsumvtxdg2size  29634  wlkepvtx  29742  wlknewwlksn  29970  wwlksnextfun  29981  wwlksnextsurj  29983  elwwlks2ons3im  30037  wwlks2onsym  30043  clwwlkf  30132  fusgreghash2wspv  30420  numclwwlk5lem  30472  grpoidinvlem3  30592  ablo32  30635  ablomuldiv  30638  ablodivdiv  30639  ablodiv32  30641  nvscom  30715  dipassr  30932  htthlem  31003  hsn0elch  31334  shscli  31403  nmopun  32100  branmfn  32191  mdslj1i  32405  mdslj2i  32406  atss  32432  chcv1  32441  dmdbr5ati  32508  snsssng  32599  ifnebib  32634  fnpreimac  32758  fcnvgreu  32760  isoun  32790  fsuppcurry1  32812  fsuppcurry2  32813  prodpr  32914  prodtp  32915  pmtrprfv2  33164  elrgspnsubrunlem2  33324  nsgmgclem  33486  nsgqusf1olem2  33489  isprmidlc  33522  ssdifidllem  33531  ssdifidlprm  33533  ssmxidllem  33548  qsdrng  33572  1arithufdlem3  33621  ordtrest2NEWlem  34082  esumsplit  34213  esumpad2  34216  esumpcvgval  34238  sigaclcu2  34280  ldgenpisyslem1  34323  volmeas  34391  mbfmco2  34425  omsmeas  34483  oddpwdc  34514  eulerpartlemgvv  34536  ballotlemfc0  34653  ballotlemfcc  34654  prodfzo03  34763  circlemethhgt  34803  bnj1109  34945  bnj1294  34975  bnj545  35053  bnj605  35065  bnj594  35070  bnj934  35093  bnj953  35097  bnj1137  35153  bnj1174  35161  bnj1388  35191  subfacp1lem4  35381  erdszelem7  35395  erdszelem8  35396  erdsze2lem2  35402  resconn  35444  cvmsdisj  35468  cvmscld  35471  satf0op  35575  mclsax  35767  climuzcnv  35869  pocnv  35961  cgrid2  36201  btwncom  36212  btwnswapid2  36216  colinearperm1  36260  colinearperm3  36261  colinearperm2  36262  colinearperm4  36263  lineext  36274  colinbtwnle  36316  broutsideof2  36320  outsideofcom  36326  linecom  36348  linerflx2  36349  lineintmo  36355  fwddifn0  36362  hfext  36381  ntruni  36525  clsint2  36527  neibastop1  36557  weiunlem  36661  bj-snsetex  37286  relowlssretop  37693  pibt2  37747  fin2solem  37941  lindsadd  37948  matunitlindflem1  37951  poimirlem4  37959  poimirlem25  37980  poimirlem32  37987  opnmbllem0  37991  mblfinlem3  37994  mbfposadd  38002  itg2addnclem3  38008  ftc1anclem6  38033  ftc1anc  38036  ac6gf  38067  heibor1lem  38144  isdrngo2  38293  unichnidl  38366  isfldidl  38403  cnf1dd  38425  membpartlem19  39249  lkrss2N  39629  elpadd0  40269  ltrnu  40581  tendoex  41435  cdlemm10N  41578  dicfnN  41643  dihmeetlem2N  41759  dihlatat  41797  lcfrlem9  42010  uzindd  42431  sticksstones1  42599  ofun  42691  nn0addcom  42921  nn0mulcom  42925  zmulcomlem  42926  fsuppind  43037  prjspner1  43073  infdesc  43090  ismrcd1  43144  isnacs3  43156  pellfundglb  43331  jm2.22  43441  jm2.23  43442  isnumbasgrplem1  43547  hbtlem6  43575  rngunsnply  43615  ordsssucim  43848  mnringmulrcld  44673  dvgrat  44757  cvgdvgrat  44758  nznngen  44761  uzmptshftfval  44791  wfac8prim  45447  rnmptlb  45690  rnmptbddlem  45691  rnmptbd2lem  45695  iccshift  45966  iooshift  45970  liminflbuz2  46261  xlimbr  46273  itgperiod  46427  fourierdlem42  46595  fourierdlem68  46620  fourierdlem93  46645  smfpimne2  47286  elprneb  47489  dfatcolem  47715  modmknepk  47828  ichim  47929  ichnfb  47937  prproropf1olem1  47975  prproropf1olem3  47977  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  2zlidl  48728  lspsslco  48925  isthincd2  49924  fullthinc  49937