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

Theorem syl5ibr 213
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 193 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 211 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5ibrcom  214  biimprd  215  dvelimvOLD  1985  pm2.61ne  2625  unineq  3534  oteqex  4390  ordtri3  4558  limelon  4585  eldifpw  4695  ssonuni  4707  onsucuni2  4754  ordzsl  4765  tfindsg  4780  findsg  4812  elrnmpt1  5059  cnveqb  5266  cnveq0  5267  relcoi1  5338  ndmfv  5695  ffvresb  5839  isomin  5996  isofrlem  5999  caovord3d  6196  frxp  6392  poxp  6394  fnwelem  6397  tfrlem1  6572  tfrlem11  6585  oacl  6715  omcl  6716  oecl  6717  oa0r  6718  om0r  6719  om1r  6722  oe1m  6724  oaordi  6725  oawordri  6729  oaass  6740  oarec  6741  omwordri  6751  odi  6758  omass  6759  oewordri  6771  oeworde  6772  oeordsuc  6773  oelim2  6774  oeoa  6776  oeoelem  6777  oeoe  6778  nnm0r  6789  nnacl  6790  nnacom  6796  nnaordi  6797  nnaass  6801  nndi  6802  nnmass  6803  nnmsucr  6804  nnmcom  6805  omabs  6826  brecop  6933  eceqoveq  6945  elpm2r  6970  map0g  6989  undifixp  7034  fundmen  7116  mapxpen  7209  mapunen  7212  php  7227  unxpdomlem2  7250  pssnn  7263  elfir  7355  wemapso2  7454  wdompwdom  7479  inf3lem1  7516  inf3lem3  7518  noinfepOLD  7548  cantnfval2  7557  cantnfp1lem3  7569  r1sdom  7633  r1tr  7635  carden2a  7786  fidomtri2  7814  prdom2  7823  infxpenlem  7828  acndom  7865  fodomacn  7870  wdomfil  7875  alephon  7883  alephordi  7888  alephle  7902  alephfplem3  7920  dfac2a  7943  kmlem9  7971  cflm  8063  cfslb  8079  cfslbn  8080  infpssrlem3  8118  infpssrlem4  8119  fin23lem21  8152  fin23lem30  8155  isf34lem7  8192  isf34lem6  8193  fin67  8208  isfin7-2  8209  fin1a2lem7  8219  fin1a2lem10  8222  iundom2g  8348  konigthlem  8376  alephreg  8390  gchdomtri  8437  wunr1om  8527  tskr1om  8575  inar1  8583  grur1a  8627  indpi  8717  genpprecl  8811  genpnmax  8817  addcmpblnr  8880  recexsrlem  8911  map2psrpr  8918  ax1rid  8969  axpre-mulgt0  8976  ltle  9096  nnmulcl  9955  nnsub  9970  nn0sub  10202  nneo  10285  uzindOLD  10296  uz11  10440  xrltle  10674  xltnegi  10734  xrsupsslem  10817  xrinfmsslem  10818  xrub  10822  supxrunb1  10830  supxrunb2  10831  om2uzuzi  11216  uzrdgxfr  11233  seqcl2  11268  seqfveq2  11272  seqshft2  11276  seqsplit  11283  seqcaopr3  11285  seqf1olem2a  11288  seqid2  11296  seqhomo  11297  ser1const  11306  m1expcl2  11330  expadd  11349  expmul  11352  faclbnd  11508  hashmap  11625  hashfacen  11630  hashf1lem1  11631  hashf1lem2  11632  hashf1  11633  seqcoll  11639  recan  12067  rexanre  12077  rlimcn2  12311  caurcvg2  12398  fsumiun  12527  efexp  12629  rpnnen2  12752  dvdstr  12810  alzdvds  12826  bitsinv1  12881  smu01lem  12924  smupval  12927  smueqlem  12929  smumullem  12931  seq1st  12989  prmdiveq  13102  odzdvds  13108  pythagtriplem2  13118  pcexp  13160  vdwlem13  13288  ramz  13320  elrestr  13583  xpsff1o  13720  subsubc  13977  frmdgsum  14734  mulgneg2  14844  mulgnnass  14845  mhmmulg  14849  symgbas  15022  gsumwrev  15089  sylow1lem1  15159  efgsfo  15298  efgred  15307  cyggexb  15435  gsum2d  15473  mulgass2  15637  lmodprop2d  15933  lspsnne2  16117  lspsneu  16122  assapropd  16313  mplcoe1  16455  mplcoe3  16456  mplcoe2  16457  ply1sclf1  16607  cnfldmulg  16656  cnfldexp  16657  restopn2  17163  cnpf2  17236  cmpfi  17393  txcn  17579  txlm  17601  xkoptsub  17607  xkopjcn  17609  ufildr  17884  cnflf  17955  fclsnei  17972  fclscmp  17983  ufilcmp  17985  cnfcf  17995  symgtgp  18052  isxms2  18368  met2ndc  18443  metustbl  18486  tngngp2  18564  clmmulg  18989  iscau4  19103  ovolunlem1a  19259  ovolicc2lem4  19283  volfiniun  19308  voliunlem1  19311  volsup  19317  dvnadd  19682  dvnres  19684  dvcobr  19699  ply1nzb  19912  plypf1  19998  dgrle  20029  coeaddlem  20034  dgrlt  20051  dvntaylp  20154  cxpmul2  20447  rlimcnp  20671  wilthlem2  20719  isnsqf  20785  musum  20843  chtub  20863  chpval2  20869  dchrisumlem1  21050  qabvexp  21187  ostthlem2  21189  usgra2edg  21268  nbusgra  21306  cusgrafilem1  21354  sizeusglecusglem1  21359  sizeusglecusg  21361  trliswlk  21403  constr2trl  21446  constr3lem6  21484  1conngra  21510  hashnbgravdg  21530  eupatrl  21538  isexid2  21761  ismndo1  21780  rngo2  21824  rngoueqz  21866  sspval  22070  nmosetre  22113  nmobndseqi  22128  nmobndseqiOLD  22129  orthcom  22458  shsva  22670  shmodsi  22739  h1datomi  22931  nmopsetretALT  23214  nmfnsetre  23228  lnopcnbd  23387  pjclem4  23550  pj3si  23558  ssmd1  23662  atom1d  23704  chjatom  23708  atcvat4i  23748  cdj3lem2a  23787  cdj3lem3a  23790  unitdivcld  24103  xrge0iifiso  24125  dya2iocuni  24427  facgam  24629  deranglem  24631  subfacp1lem6  24650  subfacval2  24652  cvmlift2lem12  24780  relexpsucr  24909  relexpsucl  24911  relexprel  24913  relexpdm  24914  relexprn  24915  relexpadd  24917  relexpindlem  24918  relexpind  24919  rtrclreclem.trans  24925  rtrclreclem.min  24926  dfrtrcl2  24927  rtrclind  24928  dfon2lem6  25168  rdgprc  25175  predpoirr  25221  predfrirr  25222  trpredlem1  25254  wfrlem14  25293  frrlem5e  25313  nodenselem8  25366  axsegconlem1  25570  ax5seglem4  25585  ax5seglem5  25586  axlowdimlem15  25609  axcontlem2  25618  axcontlem4  25620  ifscgr  25692  btwncolinear1  25717  hfelhf  25836  ordcmp  25911  findreccl  25917  nndivlub  25922  opnrebl2  26015  nn0prpw  26017  eqfnun  26114  sdclem2  26137  sdclem1  26138  prdsbnd2  26195  ismtyval  26200  rrnequiv  26235  exidreslem  26243  risci  26294  prtlem11  26406  prtlem15  26415  aovmpt4g  27734  frgra3vlem1  27753  3vfriswmgralem  27757  frconngra  27774  frgrawopreglem3  27798  bnj168  28435  bnj535  28599  bnj590  28619  bnj594  28621  bnj938  28646  bnj1118  28691  bnj1128  28697  dvelimvNEW7  28800  cvrat4  29557  lcfl6  31615
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
  Copyright terms: Public domain W3C validator