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  2714  2eu1  2729  2eu1v  2731  eqtr3  2841  elnelne1  3131  elnelne2  3132  morex  3708  psssstr  4081  reuss2  4281  reupick  4285  reximdva0  4310  falseral0  4457  rabsneu  4657  invdisjrabw  5042  opabss  5121  triun  5176  triin  5178  poirr  5478  wefrc  5542  xpcan  6026  fnfco  6536  fnressn  6913  fvtp3  6952  fvtp3g  6955  f1mpt  7011  offval  7408  ordsucuniel  7531  onzsl  7553  soex  7618  fiunlem  7635  fiun  7636  f1iun  7637  dfoprab3  7744  poxp  7814  fnwelem  7817  suppssr  7853  suppsssn  7857  suppofssd  7859  oeordsuc  8212  oelim2  8213  omsmolem  8272  ssnnfi  8729  fiint  8787  unifi  8805  indexfi  8824  iinfi  8873  unwdomg  9040  inf3lem5  9087  rankr1bg  9224  rankr1c  9242  carden2a  9387  dfac8clem  9450  dfac5lem4  9544  pwsdompw  9618  cfsuc  9671  cflim2  9677  enfin2i  9735  isf34lem4  9791  axdc4lem  9869  zornn0g  9919  uniimadomf  9959  fpwwe2lem8  10051  fpwwe2lem12  10055  fpwwe2lem13  10056  pwfseqlem1  10072  pwfseqlem5  10077  intgru  10228  addclpi  10306  addnidpi  10315  ltsonq  10383  nqpr  10428  reclem3pr  10463  recexsr  10521  supsrlem  10525  nnnn0addcl  11919  un0addcl  11922  un0mulcl  11923  nn0nndivcl  11958  nn0ge0div  12043  uzind3  12068  uzind4  12298  zsupss  12329  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  ltsubrp  12417  ltaddrp  12418  xrlttr  12525  qbtwnxr  12585  xltnegi  12601  xaddnemnf  12621  xaddnepnf  12622  xaddcom  12625  xnegdi  12633  xsubge0  12646  xrub  12697  fzind2  13147  seqof  13419  expp1  13428  expneg  13429  expcllem  13432  mulexpz  13461  expaddz  13465  expmulz  13467  faclbnd4lem3  13647  faclbnd4  13649  fi1uzind  13847  swrd00  13998  swrd0  14012  cats1un  14075  reuccatpfxs1  14101  cshw0  14148  cshwn  14151  wwlktovfo  14314  shftf  14430  sqrtdiv  14617  leabs  14651  mulcn2  14944  summolem2  15065  fsumrev2  15129  geomulcvg  15224  prodmolem2  15281  zprod  15283  prodsn  15308  prodsnf  15310  fprodle  15342  bpolydiflem  15400  bpoly2  15403  bpoly3  15404  ruclem6  15580  dvdsflip  15659  dvdsfac  15668  gcdcllem1  15840  lcmgcdlem  15942  rpexp1i  16057  hashdvds  16104  hashgcdlem  16117  phisum  16119  iserodd  16164  pcqcl  16185  pcid  16201  ismred  16865  funcpropd  17162  natpropd  17238  lubun  17725  odupos  17737  sgrpidmnd  17908  issubmd  17963  grpinvnzcl  18163  mulgneg  18238  mulgnn0z  18246  symgfixf1  18557  symgsssg  18587  symgfisg  18588  pgpssslw  18731  sylow2alem2  18735  sylow2a  18736  oddvdssubg  18967  gsumzunsnd  19068  gsumunsnfd  19069  gsum2dlem1  19082  gsum2dlem2  19083  gsumcom3  19090  ablfac1eu  19187  pgpfac1lem5  19193  gsumdixp  19351  dvdsrcl2  19392  isdrngd  19519  evlslem4  20280  coe1tmmul2  20436  cnsubrg  20597  psgnodpm  20724  mpomatmul  21047  cpmidpmat  21473  intcld  21640  neiptopnei  21732  ordtrest2lem  21803  lmss  21898  cmpcovf  21991  cncmp  21992  fincmp  21993  cmpsublem  21999  cmpsub  22000  unconn  22029  1stcfb  22045  2ndcsep  22059  refun0  22115  locfincmp  22126  1stckgenlem  22153  ptbasin  22177  ptbasfi  22181  ptunimpt  22195  ptuniconst  22198  dfac14  22218  ptcnp  22222  xkoptsub  22254  xkococnlem  22259  xkoinjcn  22287  qtopcmplem  22307  qtophmeo  22417  fbfinnfr  22441  isufil2  22508  isfcls  22609  xmetrtri  22957  xmetrtri2  22958  blssioo  23395  divcn  23468  bndth  23554  clmvscom  23686  resscdrg  23953  minveclem3  24024  finiunmbl  24137  opnmbllem  24194  ismbf2d  24233  itg2seq  24335  ellimc2  24467  limcmpt2  24474  limcres  24476  dvlem  24486  dvidlem  24505  dvrec  24544  dveflem  24568  dvlip  24582  coe1mul3  24685  dvtaylp  24950  leibpilem2  25511  leibpi  25512  wilthlem2  25638  basellem3  25652  dchreq  25826  dchrsum  25837  lgsval3  25883  lgsdir2lem4  25896  2sqlem6  25991  rpvmasumlem  26055  dchrisum0fno1  26079  rpvmasum2  26080  pntrsumbnd2  26135  ostthlem1  26195  colmid  26466  lmiisolem  26574  dfcgra2  26608  axcontlem2  26743  axcontlem7  26748  upgrex  26869  umgredg  26915  umgrpredgv  26917  umgredgne  26922  umgredgnlp  26924  usgredgppr  26970  edgssv2  26972  uspgredg2vlem  26997  usgredg2vlem1  26999  upgrres1  27087  nbuhgr2vtx1edgblem  27125  nbusgrf1o0  27143  hashnbusgrnn0  27150  iscplgredg  27191  uhgrvd00  27308  finsumvtxdg2size  27324  wlkepvtx  27434  wlknewwlksn  27657  wwlksnextfun  27668  wwlksnextsurj  27670  elwwlks2ons3im  27725  wwlks2onsym  27729  clwwlkf  27818  fusgreghash2wspv  28106  numclwwlk5lem  28158  grpoidinvlem3  28275  ablo32  28318  ablomuldiv  28321  ablodivdiv  28322  ablodiv32  28324  nvscom  28398  dipassr  28615  htthlem  28686  hsn0elch  29017  shscli  29086  nmopun  29783  branmfn  29874  mdslj1i  30088  mdslj2i  30089  atss  30115  chcv1  30124  dmdbr5ati  30191  fnpreimac  30408  fcnvgreu  30410  isoun  30429  fsuppcurry1  30453  fsuppcurry2  30454  fzne1  30503  prodpr  30535  prodtp  30536  pmtrprfv2  30725  isprmidlc  30956  ssmxidllem  30971  ordtrest2NEWlem  31158  esumsplit  31305  esumpad2  31308  esumpcvgval  31330  sigaclcu2  31372  ldgenpisyslem1  31415  volmeas  31483  mbfmco2  31516  omsmeas  31574  oddpwdc  31605  eulerpartlemgvv  31627  ballotlemfc0  31743  ballotlemfcc  31744  prodfzo03  31867  circlemethhgt  31907  bnj521  32000  bnj1109  32051  bnj1294  32082  bnj545  32160  bnj605  32172  bnj594  32177  bnj934  32200  bnj953  32204  bnj1137  32260  bnj1174  32268  bnj1388  32298  subfacp1lem4  32423  erdszelem7  32437  erdszelem8  32438  erdsze2lem2  32444  resconn  32486  cvmsdisj  32510  cvmscld  32513  satf0op  32617  mclsax  32809  climuzcnv  32907  pocnv  32992  trpredmintr  33063  fprlem2  33131  nosupno  33196  cgrid2  33457  btwncom  33468  btwnswapid2  33472  colinearperm1  33516  colinearperm3  33517  colinearperm2  33518  colinearperm4  33519  lineext  33530  colinbtwnle  33572  broutsideof2  33576  outsideofcom  33582  linecom  33604  linerflx2  33605  lineintmo  33611  fwddifn0  33618  hfext  33637  ntruni  33668  clsint2  33670  neibastop1  33700  bj-snsetex  34268  relowlssretop  34636  pibt2  34690  fin2solem  34870  lindsadd  34877  matunitlindflem1  34880  poimirlem4  34888  poimirlem25  34909  poimirlem32  34916  opnmbllem0  34920  mblfinlem3  34923  mbfposadd  34931  itg2addnclem3  34937  bddiblnc  34954  ftc1anclem6  34964  ftc1anc  34967  eqfnun  34989  ac6gf  34999  heibor1lem  35079  isdrngo2  35228  unichnidl  35301  isfldidl  35338  cnf1dd  35360  lkrss2N  36297  elpadd0  36937  ltrnu  37249  tendoex  38103  cdlemm10N  38246  dicfnN  38311  dihmeetlem2N  38427  dihlatat  38465  lcfrlem9  38678  ismrcd1  39286  isnacs3  39298  pellfundglb  39473  jm2.22  39583  jm2.23  39584  isnumbasgrplem1  39692  hbtlem6  39720  rngunsnply  39764  dvgrat  40635  cvgdvgrat  40636  nznngen  40639  uzmptshftfval  40669  rnmptlb  41504  rnmptbddlem  41505  rnmptbd2lem  41510  iccshift  41784  iooshift  41788  liminflbuz2  42086  xlimbr  42098  itgperiod  42256  fourierdlem42  42425  fourierdlem68  42450  fourierdlem93  42475  elprneb  43255  dfatcolem  43445  ichnfb  43616  prproropf1olem1  43656  prproropf1olem3  43658  rabsubmgmd  44049  2zlidl  44196  lspsslco  44483