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 218	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 594	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syl2anb  599  eupickb  2720  2eu1  2735  2eu1v  2736  eqtr3  2843  elnelne1  3133  elnelne2  3134  morex  3710  psssstr  4083  reuss2  4283  reupick  4287  reximdva0  4312  falseral0  4459  rabsneu  4665  invdisjrabw  5051  opabss  5130  triun  5185  triin  5187  poirr  5485  wefrc  5549  xpcan  6033  fnfco  6543  fnressn  6920  fvtp3  6959  fvtp3g  6962  f1mpt  7019  offval  7416  ordsucuniel  7539  onzsl  7561  soex  7626  fiunlem  7643  fiun  7644  f1iun  7645  dfoprab3  7752  poxp  7822  fnwelem  7825  suppssr  7861  suppsssn  7865  suppofssd  7867  oeordsuc  8220  oelim2  8221  omsmolem  8280  ssnnfi  8737  fiint  8795  unifi  8813  indexfi  8832  iinfi  8881  unwdomg  9048  inf3lem5  9095  rankr1bg  9232  rankr1c  9250  carden2a  9395  dfac8clem  9458  dfac5lem4  9552  pwsdompw  9626  cfsuc  9679  cflim2  9685  enfin2i  9743  isf34lem4  9799  axdc4lem  9877  zornn0g  9927  uniimadomf  9967  fpwwe2lem8  10059  fpwwe2lem12  10063  fpwwe2lem13  10064  pwfseqlem1  10080  pwfseqlem5  10085  intgru  10236  addclpi  10314  addnidpi  10323  ltsonq  10391  nqpr  10436  reclem3pr  10471  recexsr  10529  supsrlem  10533  nnnn0addcl  11928  un0addcl  11931  un0mulcl  11932  nn0nndivcl  11967  nn0ge0div  12052  uzind3  12077  uzind4  12307  zsupss  12338  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  ltsubrp  12426  ltaddrp  12427  xrlttr  12534  qbtwnxr  12594  xltnegi  12610  xaddnemnf  12630  xaddnepnf  12631  xaddcom  12634  xnegdi  12642  xsubge0  12655  xrub  12706  fzind2  13156  seqof  13428  expp1  13437  expneg  13438  expcllem  13441  mulexpz  13470  expaddz  13474  expmulz  13476  faclbnd4lem3  13656  faclbnd4  13658  fi1uzind  13856  swrd00  14006  swrd0  14020  cats1un  14083  reuccatpfxs1  14109  cshw0  14156  cshwn  14159  wwlktovfo  14322  shftf  14438  sqrtdiv  14625  leabs  14659  mulcn2  14952  summolem2  15073  fsumrev2  15137  geomulcvg  15232  prodmolem2  15289  zprod  15291  prodsn  15316  prodsnf  15318  fprodle  15350  bpolydiflem  15408  bpoly2  15411  bpoly3  15412  ruclem6  15588  dvdsflip  15667  dvdsfac  15676  gcdcllem1  15848  lcmgcdlem  15950  rpexp1i  16065  hashdvds  16112  hashgcdlem  16125  phisum  16127  iserodd  16172  pcqcl  16193  pcid  16209  ismred  16873  funcpropd  17170  natpropd  17246  lubun  17733  odupos  17745  sgrpidmnd  17916  issubmd  17971  grpinvnzcl  18171  mulgneg  18246  mulgnn0z  18254  symgfixf1  18565  symgsssg  18595  symgfisg  18596  pgpssslw  18739  sylow2alem2  18743  sylow2a  18744  oddvdssubg  18975  gsumzunsnd  19076  gsumunsnfd  19077  gsum2dlem1  19090  gsum2dlem2  19091  gsumcom3  19098  ablfac1eu  19195  pgpfac1lem5  19201  gsumdixp  19359  dvdsrcl2  19400  isdrngd  19527  evlslem4  20288  coe1tmmul2  20444  cnsubrg  20605  psgnodpm  20732  mpomatmul  21055  cpmidpmat  21481  intcld  21648  neiptopnei  21740  ordtrest2lem  21811  lmss  21906  cmpcovf  21999  cncmp  22000  fincmp  22001  cmpsublem  22007  cmpsub  22008  unconn  22037  1stcfb  22053  2ndcsep  22067  refun0  22123  locfincmp  22134  1stckgenlem  22161  ptbasin  22185  ptbasfi  22189  ptunimpt  22203  ptuniconst  22206  dfac14  22226  ptcnp  22230  xkoptsub  22262  xkococnlem  22267  xkoinjcn  22295  qtopcmplem  22315  qtophmeo  22425  fbfinnfr  22449  isufil2  22516  isfcls  22617  xmetrtri  22965  xmetrtri2  22966  blssioo  23403  divcn  23476  bndth  23562  clmvscom  23694  resscdrg  23961  minveclem3  24032  finiunmbl  24145  opnmbllem  24202  ismbf2d  24241  itg2seq  24343  ellimc2  24475  limcmpt2  24482  limcres  24484  dvlem  24494  dvidlem  24513  dvrec  24552  dveflem  24576  dvlip  24590  coe1mul3  24693  dvtaylp  24958  leibpilem2  25519  leibpi  25520  wilthlem2  25646  basellem3  25660  dchreq  25834  dchrsum  25845  lgsval3  25891  lgsdir2lem4  25904  2sqlem6  25999  rpvmasumlem  26063  dchrisum0fno1  26087  rpvmasum2  26088  pntrsumbnd2  26143  ostthlem1  26203  colmid  26474  lmiisolem  26582  dfcgra2  26616  axcontlem2  26751  axcontlem7  26756  upgrex  26877  umgredg  26923  umgrpredgv  26925  umgredgne  26930  umgredgnlp  26932  usgredgppr  26978  edgssv2  26980  uspgredg2vlem  27005  usgredg2vlem1  27007  upgrres1  27095  nbuhgr2vtx1edgblem  27133  nbusgrf1o0  27151  hashnbusgrnn0  27158  iscplgredg  27199  uhgrvd00  27316  finsumvtxdg2size  27332  wlkepvtx  27442  wlknewwlksn  27665  wwlksnextfun  27676  wwlksnextsurj  27678  elwwlks2ons3im  27733  wwlks2onsym  27737  clwwlkf  27826  fusgreghash2wspv  28114  numclwwlk5lem  28166  grpoidinvlem3  28283  ablo32  28326  ablomuldiv  28329  ablodivdiv  28330  ablodiv32  28332  nvscom  28406  dipassr  28623  htthlem  28694  hsn0elch  29025  shscli  29094  nmopun  29791  branmfn  29882  mdslj1i  30096  mdslj2i  30097  atss  30123  chcv1  30132  dmdbr5ati  30199  fnpreimac  30416  fcnvgreu  30418  isoun  30437  fsuppcurry1  30461  fsuppcurry2  30462  fzne1  30511  prodpr  30542  prodtp  30543  pmtrprfv2  30732  isprmidlc  30963  ssmxidllem  30978  ordtrest2NEWlem  31165  esumsplit  31312  esumpad2  31315  esumpcvgval  31337  sigaclcu2  31379  ldgenpisyslem1  31422  volmeas  31490  mbfmco2  31523  omsmeas  31581  oddpwdc  31612  eulerpartlemgvv  31634  ballotlemfc0  31750  ballotlemfcc  31751  prodfzo03  31874  circlemethhgt  31914  bnj521  32007  bnj1109  32058  bnj1294  32089  bnj545  32167  bnj605  32179  bnj594  32184  bnj934  32207  bnj953  32211  bnj1137  32267  bnj1174  32275  bnj1388  32305  subfacp1lem4  32430  erdszelem7  32444  erdszelem8  32445  erdsze2lem2  32451  resconn  32493  cvmsdisj  32517  cvmscld  32520  satf0op  32624  mclsax  32816  climuzcnv  32914  pocnv  32999  trpredmintr  33070  fprlem2  33138  nosupno  33203  cgrid2  33464  btwncom  33475  btwnswapid2  33479  colinearperm1  33523  colinearperm3  33524  colinearperm2  33525  colinearperm4  33526  lineext  33537  colinbtwnle  33579  broutsideof2  33583  outsideofcom  33589  linecom  33611  linerflx2  33612  lineintmo  33618  fwddifn0  33625  hfext  33644  ntruni  33675  clsint2  33677  neibastop1  33707  bj-snsetex  34278  relowlssretop  34647  pibt2  34701  fin2solem  34893  lindsadd  34900  matunitlindflem1  34903  poimirlem4  34911  poimirlem25  34932  poimirlem32  34939  opnmbllem0  34943  mblfinlem3  34946  mbfposadd  34954  itg2addnclem3  34960  bddiblnc  34977  ftc1anclem6  34987  ftc1anc  34990  eqfnun  35012  ac6gf  35022  heibor1lem  35102  isdrngo2  35251  unichnidl  35324  isfldidl  35361  cnf1dd  35383  lkrss2N  36320  elpadd0  36960  ltrnu  37272  tendoex  38126  cdlemm10N  38269  dicfnN  38334  dihmeetlem2N  38450  dihlatat  38488  lcfrlem9  38701  ismrcd1  39344  isnacs3  39356  pellfundglb  39531  jm2.22  39641  jm2.23  39642  isnumbasgrplem1  39750  hbtlem6  39778  rngunsnply  39822  dvgrat  40693  cvgdvgrat  40694  nznngen  40697  uzmptshftfval  40727  rnmptlb  41563  rnmptbddlem  41564  rnmptbd2lem  41569  iccshift  41843  iooshift  41847  liminflbuz2  42145  xlimbr  42157  itgperiod  42315  fourierdlem42  42483  fourierdlem68  42508  fourierdlem93  42533  elprneb  43313  dfatcolem  43503  ichnfb  43674  prproropf1olem1  43714  prproropf1olem3  43716  rabsubmgmd  44107  2zlidl  44254  lspsslco  44541