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

Theorem syl5ibr 223
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibr  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32bicomd 203 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 221 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186
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 187
This theorem is referenced by:  syl5ibrcom  224  biimprd  225  exdistrf  2103  pm2.61ne  2720  pm2.61neOLD  2721  unineq  3702  oteqex  4685  otel3xp  4861  elrnmpt1  5074  cnveqb  5281  cnveq0  5282  relcoi1OLD  5355  predpoirr  5397  predfrirr  5398  ordtri3  5448  limelon  5475  ndmfv  5875  ffvresb  6043  isomin  6218  isofrlem  6221  caovord3d  6468  eldifpw  6596  ssonuni  6606  onsucuni2  6654  ordzsl  6665  tfindsg  6680  findsg  6713  oteqimp  6805  frxp  6896  poxp  6898  fnwelem  6901  suppss  6935  wfrlem14  7036  tfrlem11  7093  oacl  7224  omcl  7225  oecl  7226  oa0r  7227  om0r  7228  om1r  7231  oe1m  7233  oaordi  7234  oawordri  7238  oaass  7249  oarec  7250  omwordri  7260  odi  7267  omass  7268  oewordri  7280  oeworde  7281  oeordsuc  7282  oelim2  7283  oeoa  7285  oeoelem  7286  oeoe  7287  nnm0r  7298  nnacl  7299  nnacom  7305  nnaordi  7306  nnaass  7310  nndi  7311  nnmass  7312  nnmsucr  7313  nnmcom  7314  omabs  7335  brecop  7443  eceqoveq  7455  elpm2r  7476  map0g  7498  undifixp  7545  fundmen  7629  mapxpen  7723  mapunen  7726  php  7741  unxpdomlem2  7762  pssnn  7775  elfir  7911  wemapso2OLD  8013  wemapso2lem  8014  wdompwdom  8040  inf3lem1  8080  inf3lem3  8082  cantnfval2  8122  cantnfp1lem3  8133  cantnfval2OLD  8152  cantnfp1lem3OLD  8159  r1sdom  8226  r1tr  8228  carden2a  8381  fidomtri2  8409  prdom2  8418  infxpenlem  8425  acndom  8466  fodomacn  8471  wdomfil  8476  alephon  8484  alephordi  8489  alephle  8503  alephfplem3  8521  dfac2a  8544  kmlem9  8572  cflm  8664  cfslb  8680  cfslbn  8681  infpssrlem3  8719  infpssrlem4  8720  fin23lem21  8753  fin23lem30  8756  isf34lem7  8793  isf34lem6  8794  fin67  8809  isfin7-2  8810  fin1a2lem7  8820  fin1a2lem10  8823  iundom2g  8949  konigthlem  8977  alephreg  8991  gchdomtri  9039  wunr1om  9129  tskr1om  9177  inar1  9185  grur1a  9229  indpi  9317  genpprecl  9411  genpnmax  9417  addcmpblnr  9478  recexsrlem  9512  map2psrpr  9519  ax1rid  9570  axpre-mulgt0  9577  ltle  9706  nnmulcl  10601  nnsub  10617  nn0sub  10889  nneo  10989  uz11  11151  xrltle  11410  xltnegi  11470  xrsupsslem  11553  xrinfmsslem  11554  xrub  11558  supxrunb1  11566  supxrunb2  11567  om2uzuzi  12103  uzrdgxfr  12120  seqcl2  12171  seqfveq2  12175  seqshft2  12179  seqsplit  12186  seqcaopr3  12188  seqf1olem2a  12191  seqid2  12199  seqhomo  12200  ser1const  12209  m1expcl2  12234  expadd  12254  expmul  12257  faclbnd  12414  hashmap  12544  hashfacen  12554  hashf1lem1  12555  hashf1lem2  12556  hashf1  12557  seqcoll  12563  wrdsymb0  12630  swrdnd2  12716  wrd2ind  12761  swrdccatin12lem2  12772  swrdccatin1d  12782  repswccat  12815  repswcshw  12838  cshwcshid  12853  rtrclreclem3  13044  rtrclreclem4  13045  dfrtrcl2  13046  relexpindlem  13047  relexpind  13048  rtrclind  13049  recan  13320  rexanre  13330  rlimcn2  13564  caurcvg2  13651  fsumiun  13788  efexp  14047  rpnnen2  14170  dvdstr  14229  alzdvds  14247  bitsinv1  14303  smu01lem  14346  smupval  14349  smueqlem  14351  smumullem  14353  seq1st  14411  prmdiveq  14527  odzdvds  14533  pythagtriplem2  14552  pcexp  14594  vdwlem13  14722  ramz  14754  elrestr  15045  xpsff1o  15184  subsubc  15468  clatl  16072  frmdgsum  16356  mulgneg2  16495  mulgnnass  16496  mhmmulg  16500  gsumwrev  16727  symgbas  16731  symgextf1lem  16771  symgfixelsi  16786  pmtrdifellem4  16830  sylow1lem1  16944  efgsfo  17083  efgred  17092  cyggexb  17227  gsumzres  17240  gsum2dlem2  17321  gsum2dOLD  17323  mulgass2  17569  lmodprop2d  17894  lspsnne2  18086  lspsneu  18091  assapropd  18298  mplcoe1  18449  mplcoe3  18450  mplcoe3OLD  18451  mplcoe5  18453  mplcoe2OLD  18455  ply1sclf1  18652  cnfldmulg  18772  cnfldexp  18773  zrhpsgnelbas  18930  mat1scmat  19335  restopn2  19973  cnpf2  20046  cmpfi  20203  txcn  20421  txlm  20443  xkoptsub  20449  xkopjcn  20451  ufildr  20726  cnflf  20797  fclsnei  20814  fclscmp  20825  ufilcmp  20827  cnfcf  20837  symgtgp  20894  isxms2  21245  met2ndc  21320  metustblOLD  21377  metustbl  21378  tngngp2  21460  clmmulg  21887  iscau4  22012  ovolunlem1a  22201  ovolicc2lem4  22225  volfiniun  22251  voliunlem1  22254  volsup  22260  dvnadd  22626  dvnres  22628  dvcobr  22643  ply1nzb  22817  plypf1  22903  dgrle  22934  coeaddlem  22940  dgrlt  22957  dvntaylp  23060  cxpmul2  23366  rlimcnp  23623  facgam  23723  wilthlem2  23726  isnsqf  23792  musum  23850  chtub  23870  chpval2  23876  dchrisumlem1  24057  qabvexp  24194  ostthlem2  24196  axsegconlem1  24649  ax5seglem4  24664  ax5seglem5  24665  axlowdimlem15  24688  axcontlem2  24697  axcontlem4  24699  ushgrauhgra  24732  usgra2edg  24811  cusgrafilem1  24908  sizeusglecusglem1  24913  sizeusglecusg  24915  trliswlk  24970  2trllemF  24980  constr3lem6  25078  1conngra  25104  wlkiswwlk2lem4  25123  wwlknredwwlkn0  25156  wwlkextwrd  25157  wwlkextproplem1  25170  wwlkextprop  25173  clwlkisclwwlklem2a  25214  clwwlkf1  25225  erclwwlksym  25243  eleclclwwlknlem2  25247  erclwwlknsym  25255  el2wlkonot  25298  el2spthonot  25299  hashnbgravdg  25342  eupatrl  25397  frgra3vlem1  25429  3vfriswmgralem  25433  frconngra  25450  frgrawopreglem3  25475  frg2wot1  25486  2spotiundisj  25491  usg2spot2nb  25494  usgreg2spot  25496  extwwlkfablem2  25507  numclwwlkovf2ex  25515  extwwlkfab  25519  isexid2  25754  ismndo1  25773  rngo2  25817  rngoueqz  25859  sspval  26063  nmosetre  26106  nmobndseqi  26121  nmobndseqiALT  26122  orthcom  26452  shsva  26665  shmodsi  26734  h1datomi  26926  nmopsetretALT  27208  nmfnsetre  27222  lnopcnbd  27381  pjclem4  27544  pj3si  27552  ssmd1  27656  atom1d  27698  chjatom  27702  atcvat4i  27742  cdj3lem2a  27781  cdj3lem3a  27784  disjunsn  27899  unitdivcld  28349  xrge0iifiso  28383  dya2iocuni  28744  bnj168  29125  bnj535  29288  bnj590  29308  bnj594  29310  bnj938  29335  bnj1118  29380  bnj1128  29386  deranglem  29476  subfacp1lem6  29495  subfacval2  29497  cvmlift2lem12  29624  mrsubvrs  29747  msrrcl  29768  mclsax  29794  dfon2lem6  30020  rdgprc  30027  trpredlem1  30054  frrlem5e  30108  nodenselem8  30161  ifscgr  30395  btwncolinear1  30420  hfelhf  30532  opnrebl2  30562  nn0prpw  30564  ordcmp  30692  findreccl  30698  nndivlub  30703  topdifinffinlem  31277  iooelexlt  31292  wl-mo3t  31401  eqfnun  31507  sdclem2  31530  sdclem1  31531  prdsbnd2  31586  ismtyval  31591  rrnequiv  31626  exidreslem  31634  risci  31685  prtlem11  31902  prtlem15  31911  cvrat4  32473  lcfl6  34533  iunrelexpmin1  35700  iunrelexpmin2  35704  aovmpt4g  37667  iccpartiltu  37702  iccpartgt  37707  iccpartgel  37709  zob  37729  gbepos  37825  pfxccatin12lem2  37924  f1vrnfibi  37959  ushguhg  38013  funcrngcsetc  38330  funcrngcsetcALT  38331  rhmsscrnghm  38358  funcringcsetc  38367  ellcoellss  38560  dignn0flhalflem2  38760  nn0sumshdiglemB  38764
  Copyright terms: Public domain W3C validator