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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syl2anb  598  eupickb  2638  2eu1  2653  2eu1v  2654  eqtr3OLD  2766  elnelne1  3060  elnelne2  3061  morex  3655  psssstr  4042  reuss2  4250  reupick  4253  reximdva0  4286  falseral0  4451  rabsneu  4666  invdisjrabw  5060  opabss  5139  triun  5205  triin  5207  poirr  5516  wefrc  5584  xpcan  6084  fnfco  6648  fnressn  7039  fvtp3  7081  fvtp3g  7084  f1mpt  7143  offval  7551  ordsucuniel  7680  onzsl  7702  soex  7777  fiunlem  7793  fiun  7794  f1iun  7795  dfoprab3  7903  poxp  7978  fnwelem  7981  suppssr  8021  suppssrg  8022  suppsssn  8026  suppofssd  8028  fprlem2  8126  oeordsuc  8434  oelim2  8435  omsmolem  8496  rexdif1en  8953  ssnnfi  8961  ssnnfiOLD  8962  ssfi  8965  ensymfib  8979  domnsymfi  8995  fiint  9100  unifi  9117  indexfi  9136  iinfi  9185  unwdomg  9352  inf3lem5  9399  rankr1bg  9570  rankr1c  9588  carden2a  9733  dfac8clem  9797  dfac5lem4  9891  pwsdompw  9969  cfsuc  10022  cflim2  10028  enfin2i  10086  isf34lem4  10142  axdc4lem  10220  zornn0g  10270  uniimadomf  10310  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  pwfseqlem1  10423  pwfseqlem5  10428  intgru  10579  addclpi  10657  addnidpi  10666  ltsonq  10734  nqpr  10779  reclem3pr  10814  recexsr  10872  supsrlem  10876  nnnn0addcl  12272  un0addcl  12275  un0mulcl  12276  nn0nndivcl  12313  nn0ge0div  12398  uzind3  12423  uzind4  12655  zsupss  12686  rpnnen1lem2  12726  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  ltsubrp  12775  ltaddrp  12776  xrlttr  12883  qbtwnxr  12943  xltnegi  12959  xaddnemnf  12979  xaddnepnf  12980  xaddcom  12983  xnegdi  12991  xsubge0  13004  xrub  13055  fzind2  13514  seqof  13789  expp1  13798  expneg  13799  expcllem  13802  mulexpz  13832  expaddz  13836  expmulz  13838  faclbnd4lem3  14018  faclbnd4  14020  fi1uzind  14220  swrd00  14366  swrd0  14380  cats1un  14443  reuccatpfxs1  14469  cshw0  14516  cshwn  14519  wwlktovfo  14682  shftf  14799  sqrtdiv  14986  leabs  15020  mulcn2  15314  summolem2  15437  fsumrev2  15503  geomulcvg  15597  prodmolem2  15654  zprod  15656  prodsn  15681  prodsnf  15683  fprodle  15715  bpolydiflem  15773  bpoly2  15776  bpoly3  15777  ruclem6  15953  dvdsflip  16035  dvdsfac  16044  gcdcllem1  16215  lcmgcdlem  16320  rpexp1i  16437  hashdvds  16485  hashgcdlem  16498  phisum  16500  iserodd  16545  pcqcl  16566  pcid  16583  ismred  17320  funcpropd  17625  natpropd  17703  odupos  18055  lubun  18242  sgrpidmnd  18399  issubmd  18454  grpinvnzcl  18656  mulgneg  18731  mulgnn0z  18739  symgfixf1  19054  symgsssg  19084  symgfisg  19085  pgpssslw  19228  sylow2alem2  19232  sylow2a  19233  oddvdssubg  19465  gsumzunsnd  19566  gsumunsnfd  19567  gsum2dlem1  19580  gsum2dlem2  19581  gsumcom3  19588  ablfac1eu  19685  pgpfac1lem5  19691  gsumdixp  19857  dvdsrcl2  19901  isdrngd  20025  cnsubrg  20667  psgnodpm  20802  evlslem4  21293  coe1tmmul2  21456  mpomatmul  21604  cpmidpmat  22031  intcld  22200  neiptopnei  22292  ordtrest2lem  22363  lmss  22458  cmpcovf  22551  cncmp  22552  fincmp  22553  cmpsublem  22559  cmpsub  22560  unconn  22589  1stcfb  22605  2ndcsep  22619  refun0  22675  locfincmp  22686  1stckgenlem  22713  ptbasin  22737  ptbasfi  22741  ptunimpt  22755  ptuniconst  22758  dfac14  22778  ptcnp  22782  xkoptsub  22814  xkococnlem  22819  xkoinjcn  22847  qtopcmplem  22867  qtophmeo  22977  fbfinnfr  23001  isufil2  23068  isfcls  23169  xmetrtri  23517  xmetrtri2  23518  blssioo  23967  divcn  24040  bndth  24130  clmvscom  24262  resscdrg  24531  minveclem3  24602  finiunmbl  24717  opnmbllem  24774  ismbf2d  24813  itg2seq  24916  bddiblnc  25015  ellimc2  25050  limcmpt2  25057  limcres  25059  dvlem  25069  dvidlem  25088  dvrec  25128  dveflem  25152  dvlip  25166  coe1mul3  25273  dvtaylp  25538  leibpilem2  26100  leibpi  26101  wilthlem2  26227  basellem3  26241  dchreq  26415  dchrsum  26426  lgsval3  26472  lgsdir2lem4  26485  2sqlem6  26580  rpvmasumlem  26644  dchrisum0fno1  26668  rpvmasum2  26669  pntrsumbnd2  26724  ostthlem1  26784  colmid  27058  lmiisolem  27166  dfcgra2  27200  axcontlem2  27342  axcontlem7  27347  upgrex  27471  umgredg  27517  umgrpredgv  27519  umgredgne  27524  umgredgnlp  27526  usgredgppr  27572  edgssv2  27574  uspgredg2vlem  27599  usgredg2vlem1  27601  upgrres1  27689  nbuhgr2vtx1edgblem  27727  nbusgrf1o0  27745  hashnbusgrnn0  27752  iscplgredg  27793  uhgrvd00  27910  finsumvtxdg2size  27926  wlkepvtx  28037  wlknewwlksn  28261  wwlksnextfun  28272  wwlksnextsurj  28274  elwwlks2ons3im  28328  wwlks2onsym  28332  clwwlkf  28420  fusgreghash2wspv  28708  numclwwlk5lem  28760  grpoidinvlem3  28877  ablo32  28920  ablomuldiv  28923  ablodivdiv  28924  ablodiv32  28926  nvscom  29000  dipassr  29217  htthlem  29288  hsn0elch  29619  shscli  29688  nmopun  30385  branmfn  30476  mdslj1i  30690  mdslj2i  30691  atss  30717  chcv1  30726  dmdbr5ati  30793  snsssng  30869  fnpreimac  31017  fcnvgreu  31019  isoun  31043  fsuppcurry1  31069  fsuppcurry2  31070  fzne1  31118  prodpr  31149  prodtp  31150  pmtrprfv2  31366  nsgmgclem  31605  nsgqusf1olem2  31608  isprmidlc  31632  ssmxidllem  31650  ordtrest2NEWlem  31881  esumsplit  32030  esumpad2  32033  esumpcvgval  32055  sigaclcu2  32097  ldgenpisyslem1  32140  volmeas  32208  mbfmco2  32241  omsmeas  32299  oddpwdc  32330  eulerpartlemgvv  32352  ballotlemfc0  32468  ballotlemfcc  32469  prodfzo03  32592  circlemethhgt  32632  bnj521  32725  bnj1109  32775  bnj1294  32806  bnj545  32884  bnj605  32896  bnj594  32901  bnj934  32924  bnj953  32928  bnj1137  32984  bnj1174  32992  bnj1388  33022  subfacp1lem4  33154  erdszelem7  33168  erdszelem8  33169  erdsze2lem2  33175  resconn  33217  cvmsdisj  33241  cvmscld  33244  satf0op  33348  mclsax  33540  climuzcnv  33638  pocnv  33739  poxp2  33799  nosupno  33915  cgrid2  34314  btwncom  34325  btwnswapid2  34329  colinearperm1  34373  colinearperm3  34374  colinearperm2  34375  colinearperm4  34376  lineext  34387  colinbtwnle  34429  broutsideof2  34433  outsideofcom  34439  linecom  34461  linerflx2  34462  lineintmo  34468  fwddifn0  34475  hfext  34494  ntruni  34525  clsint2  34527  neibastop1  34557  bj-snsetex  35162  relowlssretop  35543  pibt2  35597  fin2solem  35772  lindsadd  35779  matunitlindflem1  35782  poimirlem4  35790  poimirlem25  35811  poimirlem32  35818  opnmbllem0  35822  mblfinlem3  35825  mbfposadd  35833  itg2addnclem3  35839  ftc1anclem6  35864  ftc1anc  35867  eqfnun  35889  ac6gf  35899  heibor1lem  35976  isdrngo2  36125  unichnidl  36198  isfldidl  36235  cnf1dd  36257  lkrss2N  37190  elpadd0  37830  ltrnu  38142  tendoex  38996  cdlemm10N  39139  dicfnN  39204  dihmeetlem2N  39320  dihlatat  39358  lcfrlem9  39571  uzindd  39992  sticksstones1  40109  metakunt12  40143  ofun  40218  fsuppind  40286  mhphf  40292  prjspner1  40470  prjcrv0  40477  infdesc  40487  ismrcd1  40527  isnacs3  40539  pellfundglb  40714  jm2.22  40824  jm2.23  40825  isnumbasgrplem1  40933  hbtlem6  40961  rngunsnply  41005  mnringmulrcld  41853  dvgrat  41937  cvgdvgrat  41938  nznngen  41941  uzmptshftfval  41971  rnmptlb  42795  rnmptbddlem  42796  rnmptbd2lem  42801  iccshift  43063  iooshift  43067  liminflbuz2  43363  xlimbr  43375  itgperiod  43529  fourierdlem42  43697  fourierdlem68  43722  fourierdlem93  43747  elprneb  44534  dfatcolem  44758  ichim  44920  ichnfb  44928  prproropf1olem1  44966  prproropf1olem3  44968  rabsubmgmd  45356  2zlidl  45503  lspsslco  45789  isthincd2  46330  fullthinc  46338