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

Theorem syl5ibr 212
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 192 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 210 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl5ibrcom  213  biimprd  214  dvelimv  1944  pm2.61ne  2596  unineq  3495  oteqex  4341  ordtri3  4510  limelon  4537  eldifpw  4648  ssonuni  4660  onsucuni2  4707  ordzsl  4718  tfindsg  4733  findsg  4765  elrnmpt1  5010  cnveqb  5211  cnveq0  5212  relcoi1  5283  ndmfv  5635  ffvresb  5773  isomin  5921  isofrlem  5924  caovord3d  6117  frxp  6312  poxp  6314  fnwelem  6317  tfrlem1  6478  tfrlem11  6491  oacl  6621  omcl  6622  oecl  6623  oa0r  6624  om0r  6625  om1r  6628  oe1m  6630  oaordi  6631  oawordri  6635  oaass  6646  oarec  6647  omwordri  6657  odi  6664  omass  6665  oewordri  6677  oeworde  6678  oeordsuc  6679  oelim2  6680  oeoa  6682  oeoelem  6683  oeoe  6684  nnm0r  6695  nnacl  6696  nnacom  6702  nnaordi  6703  nnaass  6707  nndi  6708  nnmass  6709  nnmsucr  6710  nnmcom  6711  omabs  6732  brecop  6839  eceqoveq  6851  elpm2r  6876  map0g  6895  undifixp  6940  fundmen  7022  mapxpen  7115  mapunen  7118  php  7133  unxpdomlem2  7156  pssnn  7169  elfir  7259  wemapso2  7357  wdompwdom  7382  inf3lem1  7419  inf3lem3  7421  noinfepOLD  7451  cantnfval2  7460  cantnfp1lem3  7472  r1sdom  7536  r1tr  7538  carden2a  7689  fidomtri2  7717  prdom2  7726  infxpenlem  7731  acndom  7768  fodomacn  7773  wdomfil  7778  alephon  7786  alephordi  7791  alephle  7805  alephfplem3  7823  dfac2a  7846  kmlem9  7874  cflm  7966  cfslb  7982  cfslbn  7983  infpssrlem3  8021  infpssrlem4  8022  fin23lem21  8055  fin23lem30  8058  isf34lem7  8095  isf34lem6  8096  fin67  8111  isfin7-2  8112  fin1a2lem7  8122  fin1a2lem10  8125  iundom2g  8252  konigthlem  8280  alephreg  8294  gchdomtri  8341  wunr1om  8431  tskr1om  8479  inar1  8487  grur1a  8531  indpi  8621  genpprecl  8715  genpnmax  8721  addcmpblnr  8784  recexsrlem  8815  map2psrpr  8822  ax1rid  8873  axpre-mulgt0  8880  ltle  9000  nnmulcl  9859  nnsub  9874  nn0sub  10106  nneo  10187  uzindOLD  10198  uz11  10342  xrltle  10575  xltnegi  10635  xrsupsslem  10717  xrinfmsslem  10718  xrub  10722  supxrunb1  10730  supxrunb2  10731  om2uzuzi  11104  uzrdgxfr  11121  seqcl2  11156  seqfveq2  11160  seqshft2  11164  seqsplit  11171  seqcaopr3  11173  seqf1olem2a  11176  seqid2  11184  seqhomo  11185  ser1const  11194  m1expcl2  11218  expadd  11237  expmul  11240  faclbnd  11396  hashmap  11483  hashfacen  11488  hashf1lem1  11489  hashf1lem2  11490  hashf1  11491  seqcoll  11497  recan  11916  rexanre  11926  rlimcn2  12160  caurcvg2  12247  fsumiun  12376  efexp  12478  rpnnen2  12601  dvdstr  12659  alzdvds  12675  bitsinv1  12730  smu01lem  12773  smupval  12776  smueqlem  12778  smumullem  12780  seq1st  12838  prmdiveq  12951  odzdvds  12957  pythagtriplem2  12967  pcexp  13009  vdwlem13  13137  ramz  13169  elrestr  13432  xpsff1o  13569  subsubc  13826  frmdgsum  14583  mulgneg2  14693  mulgnnass  14694  mhmmulg  14698  symgbas  14871  gsumwrev  14938  sylow1lem1  15008  efgsfo  15147  efgred  15156  cyggexb  15284  gsum2d  15322  mulgass2  15486  lmodprop2d  15786  lspsnne2  15970  lspsneu  15975  assapropd  16166  mplcoe1  16308  mplcoe3  16309  mplcoe2  16310  ply1sclf1  16463  cnfldmulg  16512  cnfldexp  16513  restopn2  17014  cnpf2  17086  cmpfi  17241  txcn  17426  txlm  17448  xkoptsub  17454  xkopjcn  17456  ufildr  17728  cnflf  17799  fclsnei  17816  fclscmp  17827  ufilcmp  17829  cnfcf  17839  symgtgp  17886  isxms2  18096  met2ndc  18171  tngngp2  18270  clmmulg  18695  iscau4  18809  ovolunlem1a  18959  ovolicc2lem4  18983  volfiniun  19008  voliunlem1  19011  volsup  19017  dvnadd  19382  dvnres  19384  dvcobr  19399  ply1nzb  19612  plypf1  19698  dgrle  19729  coeaddlem  19734  dgrlt  19751  dvntaylp  19854  cxpmul2  20147  rlimcnp  20371  wilthlem2  20419  isnsqf  20485  musum  20543  chtub  20563  chpval2  20569  dchrisumlem1  20750  qabvexp  20887  ostthlem2  20889  isexid2  21104  ismndo1  21123  rngo2  21167  rngoueqz  21209  sspval  21413  nmosetre  21456  nmobndseqi  21471  nmobndseqiOLD  21472  orthcom  21801  shsva  22013  shmodsi  22082  h1datomi  22274  nmopsetretALT  22557  nmfnsetre  22571  lnopcnbd  22730  pjclem4  22893  pj3si  22901  ssmd1  23005  atom1d  23047  chjatom  23051  atcvat4i  23091  cdj3lem2a  23130  cdj3lem3a  23133  metustbl  23610  dya2iocuni  23897  facgam  24099  deranglem  24101  subfacp1lem6  24120  subfacval2  24122  cvmlift2lem12  24249  relexpsucr  24430  relexpsucl  24432  relexprel  24435  relexpdm  24436  relexprn  24437  relexpadd  24439  relexpindlem  24440  relexpind  24441  rtrclreclem.trans  24447  rtrclreclem.min  24448  dfrtrcl2  24449  rtrclind  24450  dfon2lem6  24702  rdgprc  24709  predpoirr  24755  predfrirr  24756  trpredlem1  24788  wfrlem14  24827  frrlem5e  24847  nodenselem8  24900  axsegconlem1  25104  ax5seglem4  25119  ax5seglem5  25120  axlowdimlem15  25143  axcontlem2  25152  axcontlem4  25154  ifscgr  25226  btwncolinear1  25251  hfelhf  25370  ordcmp  25445  findreccl  25451  nndivlub  25456  opnrebl2  25560  nn0prpw  25563  eqfnun  25711  sdclem2  25776  sdclem1  25777  prdsbnd2  25842  ismtyval  25847  rrnequiv  25882  exidreslem  25890  risci  25941  prtlem11  26057  prtlem15  26066  aovmpt4g  27389  usgra2edg  27556  nbusgra  27594  cusgrafilem1  27642  sizeusglecusglem1  27647  sizeusglecusg  27649  trliswlk  27691  constr2trl  27734  eupatrl  27763  constr3lem6  27773  1conngra  27799  hashnbgravdg  27819  frgra3vlem1  27833  3vfriswmgralem  27837  frconngra  27854  frgrawopreglem3  27879  bnj168  28520  bnj535  28684  bnj590  28704  bnj594  28706  bnj938  28731  bnj1118  28776  bnj1128  28782  dvelimvNEW7  28885  ax10lem17ALT  29192  ax9lem17  29225  cvrat4  29701  lcfl6  31759
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 177
  Copyright terms: Public domain W3C validator