MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan2b Structured version   Unicode version

Theorem sylan2b 462
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1  |-  ( ph  <->  ch )
sylan2b.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan2b  |-  ( ( ps  /\  ph )  ->  th )

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3  |-  ( ph  <->  ch )
21biimpi 187 . 2  |-  ( ph  ->  ch )
3 sylan2b.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 461 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anb  466  bm1.1  2421  eqtr3  2455  morex  3118  psssstr  3453  reuss2  3621  reupick  3625  reximdva0  3639  rabsneu  3879  opabss  4269  triun  4315  poirr  4514  wefrc  4576  ordsucuniel  4804  onzsl  4826  xpcan  5305  soex  5319  fnfco  5609  fun11iun  5695  suppssr  5864  eldmrexrnb  5877  fnressn  5918  fvtp3  5941  fvtp3g  5944  f1mpt  6007  offval  6312  dfoprab3  6403  1stconst  6435  2ndconst  6436  poxp  6458  fnwelem  6461  tfrlem2  6637  oeordsuc  6837  oelim2  6838  omsmolem  6896  fisucdomOLD  7312  ssnnfi  7328  fiint  7383  unifi  7395  indexfi  7414  iinfi  7422  unwdomg  7552  inf3lem5  7587  rankr1bg  7729  rankr1c  7747  carden2a  7853  dfac8clem  7913  dfac5lem4  8007  pwsdompw  8084  cfsuc  8137  cflim2  8143  enfin2i  8201  isf34lem4  8257  axdc4lem  8335  zornn0g  8385  uniimadomf  8420  fpwwe2lem8  8512  fpwwe2lem12  8516  fpwwe2lem13  8517  pwfseqlem1  8533  pwfseqlem5  8538  intgru  8689  addclpi  8769  addnidpi  8778  ltsonq  8846  nqpr  8891  reclem3pr  8926  recexsr  8982  supsrlem  8986  infmrcl  9987  nnnn0addcl  10251  un0addcl  10253  un0mulcl  10254  uzind3  10363  uzind3OLD  10365  uzind4  10534  zsupss  10565  rpnnen1lem1  10600  rpnnen1lem2  10601  rpnnen1lem3  10602  rpnnen1lem5  10604  ltsubrp  10643  ltaddrp  10644  xrlttr  10733  qbtwnxr  10786  xltnegi  10802  xaddnemnf  10820  xaddnepnf  10821  xaddcom  10824  xnegdi  10827  xsubge0  10840  xrub  10890  fzind2  11198  seqof  11380  expp1  11388  expneg  11389  expcllem  11392  mulexpz  11420  expaddz  11424  expmulz  11426  faclbnd4lem3  11586  faclbnd4  11588  brfi1uzind  11715  swrd00  11765  cats1un  11790  shftf  11894  sqrdiv  12071  leabs  12104  mulcn2  12389  summolem2  12510  fsumrev2  12565  geomulcvg  12653  ruclem6  12834  dvdseq  12897  dvdsfac  12904  gcdcllem1  13011  rpexp1i  13121  hashdvds  13164  iserodd  13209  pcqcl  13230  pcid  13246  ismred  13827  funcpropd  14097  natpropd  14173  latlem12  14507  clatl  14543  lubun  14550  odupos  14562  grpinvnzcl  14863  mulgneg  14908  mulgnn0z  14910  pgpssslw  15248  sylow2alem2  15252  sylow2a  15253  oddvdssubg  15470  gsumunsn  15544  gsum2d  15546  ablfac1eu  15631  pgpfac1lem5  15637  gsumdixp  15715  dvdsrcl2  15755  isdrngd  15860  evlslem4  16564  coe1tmmul2  16668  cnsubrg  16759  intcld  17104  neiptopnei  17196  ordtrest2lem  17267  lmss  17362  cmpcovf  17454  cncmp  17455  fincmp  17456  cmpsublem  17462  cmpsub  17463  uncon  17492  1stcfb  17508  2ndcsep  17522  1stckgenlem  17585  ptbasin  17609  ptbasfi  17613  ptunimpt  17627  ptuniconst  17630  dfac14  17650  ptcnp  17654  xkoptsub  17686  xkococnlem  17691  xkoinjcn  17719  qtopcmplem  17739  qtophmeo  17849  fbfinnfr  17873  isfcls  18041  psmettri2  18340  xmetrtri  18385  xmetrtri2  18386  blssioo  18826  divcn  18898  bndth  18983  resscdrg  19312  minveclem3  19330  finiunmbl  19438  opnmbllem  19493  ismbf2d  19533  itg2seq  19634  ellimc2  19764  limcmpt2  19771  limcres  19773  dvlem  19783  dvidlem  19802  dvrec  19841  dveflem  19863  dvlip  19877  coe1mul3  20022  dvtaylp  20286  leibpilem2  20781  leibpi  20782  wilthlem2  20852  basellem3  20865  dvdsflip  20967  dchreq  21042  dchrsum  21053  lgsval3  21098  lgsdir2lem4  21110  2sqlem6  21153  rpvmasumlem  21181  dchrisum0fno1  21205  rpvmasum2  21206  pntrsumbnd2  21261  ostthlem1  21321  umgraex  21358  usgraidx2vlem1  21410  nbgraf1olem3  21453  nbgraf1olem5  21455  cusconngra  21663  grpoidinvlem3  21794  ablo32  21874  ablomuldiv  21877  ablodivdiv  21878  ablodiv32  21880  nvadd12  22102  nvscom  22110  nvsubsub23  22143  dipassr  22347  htthlem  22420  hsn0elch  22750  shscli  22819  nmopun  23517  branmfn  23608  mdslj1i  23822  mdslj2i  23823  atss  23849  chcv1  23858  dmdbr5ati  23925  isoun  24089  esumsplit  24447  esumpcvgval  24468  sigaclcu2  24503  volmeas  24587  mbfmco2  24615  ballotlemfc0  24750  ballotlemfcc  24751  subfacp1lem4  24869  erdszelem7  24883  erdszelem8  24884  erdsze2lem2  24890  rescon  24933  cvmsdisj  24957  cvmscld  24960  climuzcnv  25108  prodmolem2  25261  zprod  25263  prodsn  25286  pocnv  25387  trpredmintr  25509  axcontlem2  25904  axcontlem7  25909  cgrid2  25937  btwncom  25948  btwnswapid2  25952  colinearperm1  25996  colinearperm3  25997  colinearperm2  25998  colinearperm4  25999  lineext  26010  colinbtwnle  26052  broutsideof2  26056  outsideofcom  26062  linecom  26084  linerflx2  26085  lineintmo  26091  bpolydiflem  26100  bpoly2  26103  bpoly3  26104  hfext  26124  opnmbllem0  26242  mblfinlem3  26245  mbfposadd  26254  itg2addnclem3  26258  bddiblnc  26275  ftc1anclem6  26285  ftc1anc  26288  ntruni  26330  clsint2  26332  locfincmp  26384  neibastop1  26388  eqfnun  26423  ac6gf  26434  heibor1lem  26518  isdrngo2  26574  unichnidl  26641  isfldidl  26678  ismrcd1  26752  isnacs3  26764  pellfundglb  26948  jm2.22  27066  jm2.23  27067  isnumbasgrplem1  27243  hbtlem6  27310  rngunsnply  27355  issubmd  27360  symgsssg  27385  symgfisg  27386  gsumcom3  27431  hashgcdlem  27493  phisum  27495  afv0nbfvbi  27991  nn0nndivcl  28141  nn0ge0div  28142  bnj521  29104  bnj926  29138  bnj1109  29157  bnj1294  29189  bnj545  29266  bnj605  29278  bnj594  29283  bnj934  29306  bnj953  29310  bnj1137  29364  bnj1174  29372  bnj1388  29402  lubunNEW  29771  lkrss2N  29967  elpadd0  30606  ltrnu  30918  tendoex  31772  cdlemm10N  31916  dicfnN  31981  dihmeetlem2N  32097  dihlatat  32135  lcfrlem9  32348
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator