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  2632  2eu1  2648  2eu1v  2649  elnelne1  3044  elnelne2  3045  morex  3674  psssstr  4058  reuss2  4275  reupick  4278  reximdva0  4304  falseral0OLD  4465  rabsneu  4683  invdisjrab  5082  opabss  5159  triun  5216  triin  5218  poirr  5541  wefrc  5615  xpcan  6130  fnfco  6695  eqfnun  6978  fnressn  7099  fvtp3  7139  fvtp3g  7142  f1mpt  7203  offval  7627  ordsucuniel  7762  onzsl  7784  soex  7859  fiunlem  7882  fiun  7883  f1iun  7884  dfoprab3  7994  poxp  8066  fnwelem  8069  poxp2  8081  suppssr  8133  suppssrg  8134  suppsssn  8139  suppofssd  8141  fprlem2  8239  oeordsuc  8517  oelim2  8518  omsmolem  8580  ssnnfi  9088  ssfi  9091  ensymfib  9102  domnsymfi  9118  fiint  9220  unifi  9237  indexfi  9253  iinfi  9310  unwdomg  9479  inf3lem5  9531  rankr1bg  9705  rankr1c  9723  carden2a  9868  dfac8clem  9932  dfac5lem4  10026  dfac5lem4OLD  10028  pwsdompw  10103  cfsuc  10157  cflim2  10163  enfin2i  10221  isf34lem4  10277  axdc4lem  10355  zornn0g  10405  uniimadomf  10445  fpwwe2lem7  10537  fpwwe2lem11  10541  fpwwe2lem12  10542  pwfseqlem1  10558  pwfseqlem5  10563  intgru  10714  addclpi  10792  addnidpi  10801  ltsonq  10869  nqpr  10914  reclem3pr  10949  recexsr  11007  supsrlem  11011  nnnn0addcl  12420  un0addcl  12423  un0mulcl  12424  nn0nndivcl  12462  nn0ge0div  12550  uzind3  12575  uzind4  12808  zsupss  12839  rpnnen1lem2  12879  rpnnen1lem1  12880  rpnnen1lem3  12881  rpnnen1lem5  12883  ltsubrp  12932  ltaddrp  12933  xrlttr  13043  qbtwnxr  13103  xltnegi  13119  xaddnemnf  13139  xaddnepnf  13140  xaddcom  13143  xnegdi  13151  xsubge0  13164  xrub  13215  fzne1  13508  fzind2  13692  seqof  13970  expp1  13979  expneg  13980  expcllem  13983  mulexpz  14013  expaddz  14017  expmulz  14019  faclbnd4lem3  14206  faclbnd4  14208  fi1uzind  14418  swrd00  14556  swrd0  14570  cats1un  14632  reuccatpfxs1  14658  cshw0  14705  cshwn  14708  wwlktovfo  14869  shftf  14990  sqrtdiv  15176  leabs  15210  mulcn2  15507  summolem2  15627  fsumrev2  15693  geomulcvg  15787  prodmolem2  15846  zprod  15848  prodsn  15873  prodsnf  15875  fprodle  15907  bpolydiflem  15965  bpoly2  15968  bpoly3  15969  ruclem6  16148  dvdsflip  16232  dvdsfac  16241  gcdcllem1  16414  lcmgcdlem  16521  rpexp1i  16638  hashdvds  16690  hashgcdlem  16703  phisum  16706  iserodd  16751  pcqcl  16772  pcid  16789  ismred  17508  funcpropd  17813  natpropd  17890  odupos  18236  lubun  18425  rabsubmgmd  18616  sgrpidmnd  18651  issubmd  18718  grpinvnzcl  18928  mulgneg  19009  mulgnn0z  19018  symgfixf1  19353  symgsssg  19383  symgfisg  19384  pgpssslw  19530  sylow2alem2  19534  sylow2a  19535  oddvdssubg  19771  gsumzunsnd  19872  gsumunsnfd  19873  gsum2dlem1  19886  gsum2dlem2  19887  gsumcom3  19894  ablfac1eu  19991  pgpfac1lem5  19997  gsumdixp  20241  dvdsrcl2  20288  01eq0ring  20449  isdrngd  20684  isdrngdOLD  20686  cnsubrg  21368  psgnodpm  21529  evlslem4  22014  psdmul  22084  coe1tmmul2  22193  mpomatmul  22364  cpmidpmat  22791  intcld  22958  neiptopnei  23050  ordtrest2lem  23121  lmss  23216  cmpcovf  23309  cncmp  23310  fincmp  23311  cmpsublem  23317  cmpsub  23318  unconn  23347  1stcfb  23363  2ndcsep  23377  refun0  23433  locfincmp  23444  1stckgenlem  23471  ptbasin  23495  ptbasfi  23499  ptunimpt  23513  ptuniconst  23516  dfac14  23536  ptcnp  23540  xkoptsub  23572  xkococnlem  23577  xkoinjcn  23605  qtopcmplem  23625  qtophmeo  23735  fbfinnfr  23759  isufil2  23826  isfcls  23927  xmetrtri  24273  xmetrtri2  24274  blssioo  24713  divcnOLD  24787  divcn  24789  bndth  24887  clmvscom  25020  resscdrg  25288  minveclem3  25359  finiunmbl  25475  opnmbllem  25532  ismbf2d  25571  itg2seq  25673  bddiblnc  25773  ellimc2  25808  limcmpt2  25815  limcres  25817  dvlem  25827  dvidlem  25846  dvrec  25889  dveflem  25913  dvlip  25928  coe1mul3  26034  dvtaylp  26308  leibpilem2  26881  leibpi  26882  wilthlem2  27009  basellem3  27023  dchreq  27199  dchrsum  27210  lgsval3  27256  lgsdir2lem4  27269  2sqlem6  27364  rpvmasumlem  27428  dchrisum0fno1  27452  rpvmasum2  27453  pntrsumbnd2  27508  ostthlem1  27568  nosupno  27645  negsbdaylem  28001  expsp1  28355  colmid  28669  lmiisolem  28777  dfcgra2  28811  axcontlem2  28947  axcontlem7  28952  upgrex  29074  umgredg  29120  umgrpredgv  29122  umgredgne  29127  umgredgnlp  29129  usgredgppr  29178  edgssv2  29180  uspgredg2vlem  29205  usgredg2vlem1  29207  upgrres1  29295  nbuhgr2vtx1edgblem  29333  nbusgrf1o0  29351  hashnbusgrnn0  29358  iscplgredg  29399  uhgrvd00  29517  finsumvtxdg2size  29533  wlkepvtx  29641  wlknewwlksn  29869  wwlksnextfun  29880  wwlksnextsurj  29882  elwwlks2ons3im  29936  wwlks2onsym  29942  clwwlkf  30031  fusgreghash2wspv  30319  numclwwlk5lem  30371  grpoidinvlem3  30490  ablo32  30533  ablomuldiv  30536  ablodivdiv  30537  ablodiv32  30539  nvscom  30613  dipassr  30830  htthlem  30901  hsn0elch  31232  shscli  31301  nmopun  31998  branmfn  32089  mdslj1i  32303  mdslj2i  32304  atss  32330  chcv1  32339  dmdbr5ati  32406  snsssng  32498  ifnebib  32533  fnpreimac  32657  fcnvgreu  32659  isoun  32689  fsuppcurry1  32713  fsuppcurry2  32714  prodpr  32816  prodtp  32817  pmtrprfv2  33066  elrgspnsubrunlem2  33224  nsgmgclem  33385  nsgqusf1olem2  33388  isprmidlc  33421  ssdifidllem  33430  ssdifidlprm  33432  ssmxidllem  33447  qsdrng  33471  1arithufdlem3  33520  ordtrest2NEWlem  33958  esumsplit  34089  esumpad2  34092  esumpcvgval  34114  sigaclcu2  34156  ldgenpisyslem1  34199  volmeas  34267  mbfmco2  34301  omsmeas  34359  oddpwdc  34390  eulerpartlemgvv  34412  ballotlemfc0  34529  ballotlemfcc  34530  prodfzo03  34639  circlemethhgt  34679  bnj1109  34821  bnj1294  34852  bnj545  34930  bnj605  34942  bnj594  34947  bnj934  34970  bnj953  34974  bnj1137  35030  bnj1174  35038  bnj1388  35068  subfacp1lem4  35250  erdszelem7  35264  erdszelem8  35265  erdsze2lem2  35271  resconn  35313  cvmsdisj  35337  cvmscld  35340  satf0op  35444  mclsax  35636  climuzcnv  35738  pocnv  35830  cgrid2  36070  btwncom  36081  btwnswapid2  36085  colinearperm1  36129  colinearperm3  36130  colinearperm2  36131  colinearperm4  36132  lineext  36143  colinbtwnle  36185  broutsideof2  36189  outsideofcom  36195  linecom  36217  linerflx2  36218  lineintmo  36224  fwddifn0  36231  hfext  36250  ntruni  36394  clsint2  36396  neibastop1  36426  weiunlem2  36530  bj-snsetex  37030  relowlssretop  37430  pibt2  37484  fin2solem  37669  lindsadd  37676  matunitlindflem1  37679  poimirlem4  37687  poimirlem25  37708  poimirlem32  37715  opnmbllem0  37719  mblfinlem3  37722  mbfposadd  37730  itg2addnclem3  37736  ftc1anclem6  37761  ftc1anc  37764  ac6gf  37795  heibor1lem  37872  isdrngo2  38021  unichnidl  38094  isfldidl  38131  cnf1dd  38153  membpartlem19  38932  lkrss2N  39291  elpadd0  39931  ltrnu  40243  tendoex  41097  cdlemm10N  41240  dicfnN  41305  dihmeetlem2N  41421  dihlatat  41459  lcfrlem9  41672  uzindd  42093  sticksstones1  42262  ofun  42357  nn0addcom  42583  nn0mulcom  42587  zmulcomlem  42588  fsuppind  42711  prjspner1  42747  infdesc  42764  ismrcd1  42818  isnacs3  42830  pellfundglb  43005  jm2.22  43115  jm2.23  43116  isnumbasgrplem1  43221  hbtlem6  43249  rngunsnply  43289  ordsssucim  43522  mnringmulrcld  44348  dvgrat  44432  cvgdvgrat  44433  nznngen  44436  uzmptshftfval  44466  wfac8prim  45122  rnmptlb  45367  rnmptbddlem  45368  rnmptbd2lem  45372  iccshift  45645  iooshift  45649  liminflbuz2  45940  xlimbr  45952  itgperiod  46106  fourierdlem42  46274  fourierdlem68  46299  fourierdlem93  46324  smfpimne2  46965  elprneb  47156  dfatcolem  47382  modmknepk  47489  ichim  47584  ichnfb  47592  prproropf1olem1  47630  prproropf1olem3  47632  gpgnbgrvtx0  48201  gpgnbgrvtx1  48202  2zlidl  48367  lspsslco  48565  isthincd2  49565  fullthinc  49578