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

Theorem syl5ibr 221
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 201 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 219 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  syl5ibrcom  222  biimprd  223  exdistrf  2076  pm2.61ne  2772  pm2.61neOLD  2773  unineq  3755  oteqex  4749  ordtri3  4923  limelon  4950  otel3xp  5044  elrnmpt1  5261  cnveqb  5468  cnveq0  5469  relcoi1  5542  ndmfv  5896  ffvresb  6063  isomin  6234  isofrlem  6237  caovord3d  6484  eldifpw  6611  ssonuni  6621  onsucuni2  6668  ordzsl  6679  tfindsg  6694  findsg  6726  oteqimp  6818  frxp  6909  poxp  6911  fnwelem  6914  suppss  6948  tfrlem11  7075  oacl  7203  omcl  7204  oecl  7205  oa0r  7206  om0r  7207  om1r  7210  oe1m  7212  oaordi  7213  oawordri  7217  oaass  7228  oarec  7229  omwordri  7239  odi  7246  omass  7247  oewordri  7259  oeworde  7260  oeordsuc  7261  oelim2  7262  oeoa  7264  oeoelem  7265  oeoe  7266  nnm0r  7277  nnacl  7278  nnacom  7284  nnaordi  7285  nnaass  7289  nndi  7290  nnmass  7291  nnmsucr  7292  nnmcom  7293  omabs  7314  brecop  7422  eceqoveq  7434  elpm2r  7455  map0g  7477  undifixp  7524  fundmen  7608  mapxpen  7702  mapunen  7705  php  7720  unxpdomlem2  7744  pssnn  7757  elfir  7893  wemapso2OLD  7995  wemapso2lem  7996  wdompwdom  8022  inf3lem1  8062  inf3lem3  8064  noinfepOLD  8094  cantnfval2  8105  cantnfp1lem3  8116  cantnfval2OLD  8135  cantnfp1lem3OLD  8142  r1sdom  8209  r1tr  8211  carden2a  8364  fidomtri2  8392  prdom2  8401  infxpenlem  8408  acndom  8449  fodomacn  8454  wdomfil  8459  alephon  8467  alephordi  8472  alephle  8486  alephfplem3  8504  dfac2a  8527  kmlem9  8555  cflm  8647  cfslb  8663  cfslbn  8664  infpssrlem3  8702  infpssrlem4  8703  fin23lem21  8736  fin23lem30  8739  isf34lem7  8776  isf34lem6  8777  fin67  8792  isfin7-2  8793  fin1a2lem7  8803  fin1a2lem10  8806  iundom2g  8932  konigthlem  8960  alephreg  8974  gchdomtri  9024  wunr1om  9114  tskr1om  9162  inar1  9170  grur1a  9214  indpi  9302  genpprecl  9396  genpnmax  9402  addcmpblnr  9463  recexsrlem  9497  map2psrpr  9504  ax1rid  9555  axpre-mulgt0  9562  ltle  9690  nnmulcl  10579  nnsub  10595  nn0sub  10867  nneo  10967  uzindOLD  10978  uz11  11128  xrltle  11380  xltnegi  11440  xrsupsslem  11523  xrinfmsslem  11524  xrub  11528  supxrunb1  11536  supxrunb2  11537  om2uzuzi  12063  uzrdgxfr  12080  seqcl2  12128  seqfveq2  12132  seqshft2  12136  seqsplit  12143  seqcaopr3  12145  seqf1olem2a  12148  seqid2  12156  seqhomo  12157  ser1const  12166  m1expcl2  12191  expadd  12211  expmul  12214  faclbnd  12371  hashmap  12497  hashfacen  12507  hashf1lem1  12508  hashf1lem2  12509  hashf1  12510  seqcoll  12516  wrdsymb0  12583  swrdnd2  12669  wrd2ind  12715  swrdccatin12lem2  12726  swrdccatin1d  12736  repswccat  12769  repswcshw  12792  cshwcshid  12807  recan  13181  rexanre  13191  rlimcn2  13425  caurcvg2  13512  fsumiun  13647  efexp  13848  rpnnen2  13971  dvdstr  14030  alzdvds  14048  bitsinv1  14104  smu01lem  14147  smupval  14150  smueqlem  14152  smumullem  14154  seq1st  14212  prmdiveq  14328  odzdvds  14334  pythagtriplem2  14353  pcexp  14395  vdwlem13  14523  ramz  14555  elrestr  14846  xpsff1o  14985  subsubc  15269  clatl  15873  frmdgsum  16157  mulgneg2  16296  mulgnnass  16297  mhmmulg  16301  gsumwrev  16528  symgbas  16532  symgextf1lem  16572  symgfixelsi  16587  pmtrdifellem4  16631  sylow1lem1  16745  efgsfo  16884  efgred  16893  cyggexb  17028  gsumzres  17041  gsum2dlem2  17125  gsum2dOLD  17127  mulgass2  17374  lmodprop2d  17699  lspsnne2  17891  lspsneu  17896  assapropd  18103  mplcoe1  18254  mplcoe3  18255  mplcoe3OLD  18256  mplcoe5  18258  mplcoe2OLD  18260  ply1sclf1  18457  cnfldmulg  18577  cnfldexp  18578  zrhpsgnelbas  18757  mat1scmat  19168  restopn2  19805  cnpf2  19878  cmpfi  20035  txcn  20253  txlm  20275  xkoptsub  20281  xkopjcn  20283  ufildr  20558  cnflf  20629  fclsnei  20646  fclscmp  20657  ufilcmp  20659  cnfcf  20669  symgtgp  20726  isxms2  21077  met2ndc  21152  metustblOLD  21209  metustbl  21210  tngngp2  21292  clmmulg  21719  iscau4  21844  ovolunlem1a  22033  ovolicc2lem4  22057  volfiniun  22083  voliunlem1  22086  volsup  22092  dvnadd  22458  dvnres  22460  dvcobr  22475  ply1nzb  22649  plypf1  22735  dgrle  22766  coeaddlem  22772  dgrlt  22789  dvntaylp  22892  cxpmul2  23196  rlimcnp  23421  wilthlem2  23469  isnsqf  23535  musum  23593  chtub  23613  chpval2  23619  dchrisumlem1  23800  qabvexp  23937  ostthlem2  23939  axsegconlem1  24347  ax5seglem4  24362  ax5seglem5  24363  axlowdimlem15  24386  axcontlem2  24395  axcontlem4  24397  ushgrauhgra  24430  usgra2edg  24509  cusgrafilem1  24606  sizeusglecusglem1  24611  sizeusglecusg  24613  trliswlk  24668  2trllemF  24678  constr3lem6  24776  1conngra  24802  wlkiswwlk2lem4  24821  wwlknredwwlkn0  24854  wwlkextwrd  24855  wwlkextproplem1  24868  wwlkextprop  24871  clwlkisclwwlklem2a  24912  clwwlkf1  24923  erclwwlksym  24941  eleclclwwlknlem2  24945  erclwwlknsym  24953  el2wlkonot  24996  el2spthonot  24997  hashnbgravdg  25040  eupatrl  25095  frgra3vlem1  25127  3vfriswmgralem  25131  frconngra  25148  frgrawopreglem3  25173  frg2wot1  25184  2spotiundisj  25189  usg2spot2nb  25192  usgreg2spot  25194  extwwlkfablem2  25205  numclwwlkovf2ex  25213  extwwlkfab  25217  isexid2  25454  ismndo1  25473  rngo2  25517  rngoueqz  25559  sspval  25763  nmosetre  25806  nmobndseqi  25821  nmobndseqiALT  25822  orthcom  26152  shsva  26365  shmodsi  26434  h1datomi  26626  nmopsetretALT  26909  nmfnsetre  26923  lnopcnbd  27082  pjclem4  27245  pj3si  27253  ssmd1  27357  atom1d  27399  chjatom  27403  atcvat4i  27443  cdj3lem2a  27482  cdj3lem3a  27485  disjunsn  27593  unitdivcld  28044  xrge0iifiso  28078  dya2iocuni  28427  facgam  28805  deranglem  28807  subfacp1lem6  28826  subfacval2  28828  cvmlift2lem12  28956  mrsubvrs  29079  msrrcl  29100  mclsax  29126  relexpindlem  29280  relexpind  29281  rtrclreclem.trans  29287  rtrclreclem.min  29288  dfrtrcl2  29289  rtrclind  29290  dfon2lem6  29437  rdgprc  29444  predpoirr  29494  predfrirr  29495  trpredlem1  29527  wfrlem14  29573  frrlem5e  29612  nodenselem8  29665  ifscgr  29899  btwncolinear1  29924  hfelhf  30043  ordcmp  30117  findreccl  30123  nndivlub  30128  wl-mo3t  30226  opnrebl2  30344  nn0prpw  30346  eqfnun  30417  sdclem2  30440  sdclem1  30441  prdsbnd2  30496  ismtyval  30501  rrnequiv  30536  exidreslem  30544  risci  30595  prtlem11  30812  prtlem15  30821  aovmpt4g  32489  pfxccatin12lem2  32542  f1vrnfibi  32577  ushguhg  32633  funcrngcsetc  32950  funcrngcsetcALT  32951  rhmsscrnghm  32978  funcringcsetc  32987  ellcoellss  33180  bnj168  33928  bnj535  34091  bnj590  34111  bnj594  34113  bnj938  34138  bnj1118  34183  bnj1128  34189  cvrat4  35310  lcfl6  37370
  Copyright terms: Public domain W3C validator