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  2630  2eu1  2646  2eu1v  2647  elnelne1  3043  elnelne2  3044  morex  3678  psssstr  4059  reuss2  4276  reupick  4279  reximdva0  4305  falseral0  4466  rabsneu  4682  invdisjrab  5078  opabss  5155  triun  5212  triin  5214  poirr  5536  wefrc  5610  xpcan  6123  fnfco  6688  eqfnun  6970  fnressn  7091  fvtp3  7131  fvtp3g  7134  f1mpt  7195  offval  7619  ordsucuniel  7754  onzsl  7776  soex  7851  fiunlem  7874  fiun  7875  f1iun  7876  dfoprab3  7986  poxp  8058  fnwelem  8061  poxp2  8073  suppssr  8125  suppssrg  8126  suppsssn  8131  suppofssd  8133  fprlem2  8231  oeordsuc  8509  oelim2  8510  omsmolem  8572  ssnnfi  9079  ssfi  9082  ensymfib  9093  domnsymfi  9109  fiint  9211  unifi  9228  indexfi  9244  iinfi  9301  unwdomg  9470  inf3lem5  9522  rankr1bg  9696  rankr1c  9714  carden2a  9859  dfac8clem  9923  dfac5lem4  10017  dfac5lem4OLD  10019  pwsdompw  10094  cfsuc  10148  cflim2  10154  enfin2i  10212  isf34lem4  10268  axdc4lem  10346  zornn0g  10396  uniimadomf  10436  fpwwe2lem7  10528  fpwwe2lem11  10532  fpwwe2lem12  10533  pwfseqlem1  10549  pwfseqlem5  10554  intgru  10705  addclpi  10783  addnidpi  10792  ltsonq  10860  nqpr  10905  reclem3pr  10940  recexsr  10998  supsrlem  11002  nnnn0addcl  12411  un0addcl  12414  un0mulcl  12415  nn0nndivcl  12453  nn0ge0div  12542  uzind3  12567  uzind4  12804  zsupss  12835  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  ltsubrp  12928  ltaddrp  12929  xrlttr  13039  qbtwnxr  13099  xltnegi  13115  xaddnemnf  13135  xaddnepnf  13136  xaddcom  13139  xnegdi  13147  xsubge0  13160  xrub  13211  fzne1  13504  fzind2  13688  seqof  13966  expp1  13975  expneg  13976  expcllem  13979  mulexpz  14009  expaddz  14013  expmulz  14015  faclbnd4lem3  14202  faclbnd4  14204  fi1uzind  14414  swrd00  14552  swrd0  14566  cats1un  14628  reuccatpfxs1  14654  cshw0  14701  cshwn  14704  wwlktovfo  14865  shftf  14986  sqrtdiv  15172  leabs  15206  mulcn2  15503  summolem2  15623  fsumrev2  15689  geomulcvg  15783  prodmolem2  15842  zprod  15844  prodsn  15869  prodsnf  15871  fprodle  15903  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  ruclem6  16144  dvdsflip  16228  dvdsfac  16237  gcdcllem1  16410  lcmgcdlem  16517  rpexp1i  16634  hashdvds  16686  hashgcdlem  16699  phisum  16702  iserodd  16747  pcqcl  16768  pcid  16785  ismred  17504  funcpropd  17809  natpropd  17886  odupos  18232  lubun  18421  rabsubmgmd  18612  sgrpidmnd  18647  issubmd  18714  grpinvnzcl  18924  mulgneg  19005  mulgnn0z  19014  symgfixf1  19350  symgsssg  19380  symgfisg  19381  pgpssslw  19527  sylow2alem2  19531  sylow2a  19532  oddvdssubg  19768  gsumzunsnd  19869  gsumunsnfd  19870  gsum2dlem1  19883  gsum2dlem2  19884  gsumcom3  19891  ablfac1eu  19988  pgpfac1lem5  19994  gsumdixp  20238  dvdsrcl2  20285  01eq0ring  20446  isdrngd  20681  isdrngdOLD  20683  cnsubrg  21365  psgnodpm  21526  evlslem4  22012  psdmul  22082  coe1tmmul2  22191  mpomatmul  22362  cpmidpmat  22789  intcld  22956  neiptopnei  23048  ordtrest2lem  23119  lmss  23214  cmpcovf  23307  cncmp  23308  fincmp  23309  cmpsublem  23315  cmpsub  23316  unconn  23345  1stcfb  23361  2ndcsep  23375  refun0  23431  locfincmp  23442  1stckgenlem  23469  ptbasin  23493  ptbasfi  23497  ptunimpt  23511  ptuniconst  23514  dfac14  23534  ptcnp  23538  xkoptsub  23570  xkococnlem  23575  xkoinjcn  23603  qtopcmplem  23623  qtophmeo  23733  fbfinnfr  23757  isufil2  23824  isfcls  23925  xmetrtri  24271  xmetrtri2  24272  blssioo  24711  divcnOLD  24785  divcn  24787  bndth  24885  clmvscom  25018  resscdrg  25286  minveclem3  25357  finiunmbl  25473  opnmbllem  25530  ismbf2d  25569  itg2seq  25671  bddiblnc  25771  ellimc2  25806  limcmpt2  25813  limcres  25815  dvlem  25825  dvidlem  25844  dvrec  25887  dveflem  25911  dvlip  25926  coe1mul3  26032  dvtaylp  26306  leibpilem2  26879  leibpi  26880  wilthlem2  27007  basellem3  27021  dchreq  27197  dchrsum  27208  lgsval3  27254  lgsdir2lem4  27267  2sqlem6  27362  rpvmasumlem  27426  dchrisum0fno1  27450  rpvmasum2  27451  pntrsumbnd2  27506  ostthlem1  27566  nosupno  27643  negsbdaylem  27999  expsp1  28353  colmid  28667  lmiisolem  28775  dfcgra2  28809  axcontlem2  28944  axcontlem7  28949  upgrex  29071  umgredg  29117  umgrpredgv  29119  umgredgne  29124  umgredgnlp  29126  usgredgppr  29175  edgssv2  29177  uspgredg2vlem  29202  usgredg2vlem1  29204  upgrres1  29292  nbuhgr2vtx1edgblem  29330  nbusgrf1o0  29348  hashnbusgrnn0  29355  iscplgredg  29396  uhgrvd00  29514  finsumvtxdg2size  29530  wlkepvtx  29638  wlknewwlksn  29866  wwlksnextfun  29877  wwlksnextsurj  29879  elwwlks2ons3im  29933  wwlks2onsym  29937  clwwlkf  30025  fusgreghash2wspv  30313  numclwwlk5lem  30365  grpoidinvlem3  30484  ablo32  30527  ablomuldiv  30530  ablodivdiv  30531  ablodiv32  30533  nvscom  30607  dipassr  30824  htthlem  30895  hsn0elch  31226  shscli  31295  nmopun  31992  branmfn  32083  mdslj1i  32297  mdslj2i  32298  atss  32324  chcv1  32333  dmdbr5ati  32400  snsssng  32492  ifnebib  32527  fnpreimac  32651  fcnvgreu  32653  isoun  32681  fsuppcurry1  32705  fsuppcurry2  32706  prodpr  32807  prodtp  32808  pmtrprfv2  33055  elrgspnsubrunlem2  33213  nsgmgclem  33374  nsgqusf1olem2  33377  isprmidlc  33410  ssdifidllem  33419  ssdifidlprm  33421  ssmxidllem  33436  qsdrng  33460  1arithufdlem3  33509  ordtrest2NEWlem  33933  esumsplit  34064  esumpad2  34067  esumpcvgval  34089  sigaclcu2  34131  ldgenpisyslem1  34174  volmeas  34242  mbfmco2  34276  omsmeas  34334  oddpwdc  34365  eulerpartlemgvv  34387  ballotlemfc0  34504  ballotlemfcc  34505  prodfzo03  34614  circlemethhgt  34654  bnj1109  34796  bnj1294  34827  bnj545  34905  bnj605  34917  bnj594  34922  bnj934  34945  bnj953  34949  bnj1137  35005  bnj1174  35013  bnj1388  35043  subfacp1lem4  35225  erdszelem7  35239  erdszelem8  35240  erdsze2lem2  35246  resconn  35288  cvmsdisj  35312  cvmscld  35315  satf0op  35419  mclsax  35611  climuzcnv  35713  pocnv  35805  cgrid2  36043  btwncom  36054  btwnswapid2  36058  colinearperm1  36102  colinearperm3  36103  colinearperm2  36104  colinearperm4  36105  lineext  36116  colinbtwnle  36158  broutsideof2  36162  outsideofcom  36168  linecom  36190  linerflx2  36191  lineintmo  36197  fwddifn0  36204  hfext  36223  ntruni  36367  clsint2  36369  neibastop1  36399  weiunlem2  36503  bj-snsetex  37003  relowlssretop  37403  pibt2  37457  fin2solem  37652  lindsadd  37659  matunitlindflem1  37662  poimirlem4  37670  poimirlem25  37691  poimirlem32  37698  opnmbllem0  37702  mblfinlem3  37705  mbfposadd  37713  itg2addnclem3  37719  ftc1anclem6  37744  ftc1anc  37747  ac6gf  37778  heibor1lem  37855  isdrngo2  38004  unichnidl  38077  isfldidl  38114  cnf1dd  38136  membpartlem19  38855  lkrss2N  39214  elpadd0  39854  ltrnu  40166  tendoex  41020  cdlemm10N  41163  dicfnN  41228  dihmeetlem2N  41344  dihlatat  41382  lcfrlem9  41595  uzindd  42016  sticksstones1  42185  ofun  42275  nn0addcom  42501  nn0mulcom  42505  zmulcomlem  42506  fsuppind  42629  prjspner1  42665  infdesc  42682  ismrcd1  42737  isnacs3  42749  pellfundglb  42924  jm2.22  43034  jm2.23  43035  isnumbasgrplem1  43140  hbtlem6  43168  rngunsnply  43208  ordsssucim  43441  mnringmulrcld  44267  dvgrat  44351  cvgdvgrat  44352  nznngen  44355  uzmptshftfval  44385  wfac8prim  45041  rnmptlb  45286  rnmptbddlem  45287  rnmptbd2lem  45291  iccshift  45564  iooshift  45568  liminflbuz2  45859  xlimbr  45871  itgperiod  46025  fourierdlem42  46193  fourierdlem68  46218  fourierdlem93  46243  smfpimne2  46884  elprneb  47066  dfatcolem  47292  modmknepk  47399  ichim  47494  ichnfb  47502  prproropf1olem1  47540  prproropf1olem3  47542  gpgnbgrvtx0  48111  gpgnbgrvtx1  48112  2zlidl  48277  lspsslco  48475  isthincd2  49475  fullthinc  49488