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

Theorem syl5ibr 214
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 194 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 212 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl5ibrcom  215  biimprd  216  dvelimvOLD  2029  exdistrf  2067  pm2.61ne  2681  unineq  3593  oteqex  4451  ordtri3  4619  limelon  4646  eldifpw  4757  ssonuni  4769  onsucuni2  4816  ordzsl  4827  tfindsg  4842  findsg  4874  elrnmpt1  5121  cnveqb  5328  cnveq0  5329  relcoi1  5400  ndmfv  5757  ffvresb  5902  isomin  6059  isofrlem  6062  caovord3d  6259  frxp  6458  poxp  6460  fnwelem  6463  tfrlem1  6638  tfrlem11  6651  oacl  6781  omcl  6782  oecl  6783  oa0r  6784  om0r  6785  om1r  6788  oe1m  6790  oaordi  6791  oawordri  6795  oaass  6806  oarec  6807  omwordri  6817  odi  6824  omass  6825  oewordri  6837  oeworde  6838  oeordsuc  6839  oelim2  6840  oeoa  6842  oeoelem  6843  oeoe  6844  nnm0r  6855  nnacl  6856  nnacom  6862  nnaordi  6863  nnaass  6867  nndi  6868  nnmass  6869  nnmsucr  6870  nnmcom  6871  omabs  6892  brecop  6999  eceqoveq  7011  elpm2r  7036  map0g  7055  undifixp  7100  fundmen  7182  mapxpen  7275  mapunen  7278  php  7293  unxpdomlem2  7316  pssnn  7329  elfir  7422  wemapso2  7523  wdompwdom  7548  inf3lem1  7585  inf3lem3  7587  noinfepOLD  7617  cantnfval2  7626  cantnfp1lem3  7638  r1sdom  7702  r1tr  7704  carden2a  7855  fidomtri2  7883  prdom2  7892  infxpenlem  7897  acndom  7934  fodomacn  7939  wdomfil  7944  alephon  7952  alephordi  7957  alephle  7971  alephfplem3  7989  dfac2a  8012  kmlem9  8040  cflm  8132  cfslb  8148  cfslbn  8149  infpssrlem3  8187  infpssrlem4  8188  fin23lem21  8221  fin23lem30  8224  isf34lem7  8261  isf34lem6  8262  fin67  8277  isfin7-2  8278  fin1a2lem7  8288  fin1a2lem10  8291  iundom2g  8417  konigthlem  8445  alephreg  8459  gchdomtri  8506  wunr1om  8596  tskr1om  8644  inar1  8652  grur1a  8696  indpi  8786  genpprecl  8880  genpnmax  8886  addcmpblnr  8949  recexsrlem  8980  map2psrpr  8987  ax1rid  9038  axpre-mulgt0  9045  ltle  9165  nnmulcl  10025  nnsub  10040  nn0sub  10272  nneo  10355  uzindOLD  10366  uz11  10510  xrltle  10744  xltnegi  10804  xrsupsslem  10887  xrinfmsslem  10888  xrub  10892  supxrunb1  10900  supxrunb2  10901  om2uzuzi  11291  uzrdgxfr  11308  seqcl2  11343  seqfveq2  11347  seqshft2  11351  seqsplit  11358  seqcaopr3  11360  seqf1olem2a  11363  seqid2  11371  seqhomo  11372  ser1const  11381  m1expcl2  11405  expadd  11424  expmul  11427  faclbnd  11583  hashmap  11700  hashfacen  11705  hashf1lem1  11706  hashf1lem2  11707  hashf1  11708  seqcoll  11714  recan  12142  rexanre  12152  rlimcn2  12386  caurcvg2  12473  fsumiun  12602  efexp  12704  rpnnen2  12827  dvdstr  12885  alzdvds  12901  bitsinv1  12956  smu01lem  12999  smupval  13002  smueqlem  13004  smumullem  13006  seq1st  13064  prmdiveq  13177  odzdvds  13183  pythagtriplem2  13193  pcexp  13235  vdwlem13  13363  ramz  13395  elrestr  13658  xpsff1o  13795  subsubc  14052  frmdgsum  14809  mulgneg2  14919  mulgnnass  14920  mhmmulg  14924  symgbas  15097  gsumwrev  15164  sylow1lem1  15234  efgsfo  15373  efgred  15382  cyggexb  15510  gsum2d  15548  mulgass2  15712  lmodprop2d  16008  lspsnne2  16192  lspsneu  16197  assapropd  16388  mplcoe1  16530  mplcoe3  16531  mplcoe2  16532  ply1sclf1  16682  cnfldmulg  16735  cnfldexp  16736  restopn2  17243  cnpf2  17316  cmpfi  17473  txcn  17660  txlm  17682  xkoptsub  17688  xkopjcn  17690  ufildr  17965  cnflf  18036  fclsnei  18053  fclscmp  18064  ufilcmp  18066  cnfcf  18076  symgtgp  18133  isxms2  18480  met2ndc  18555  metustblOLD  18612  metustbl  18613  tngngp2  18695  clmmulg  19120  iscau4  19234  ovolunlem1a  19394  ovolicc2lem4  19418  volfiniun  19443  voliunlem1  19446  volsup  19452  dvnadd  19817  dvnres  19819  dvcobr  19834  ply1nzb  20047  plypf1  20133  dgrle  20164  coeaddlem  20169  dgrlt  20186  dvntaylp  20289  cxpmul2  20582  rlimcnp  20806  wilthlem2  20854  isnsqf  20920  musum  20978  chtub  20998  chpval2  21004  dchrisumlem1  21185  qabvexp  21322  ostthlem2  21324  usgra2edg  21404  cusgrafilem1  21490  sizeusglecusglem1  21495  sizeusglecusg  21497  trliswlk  21541  2trllemF  21551  constr3lem6  21638  1conngra  21664  hashnbgravdg  21684  eupatrl  21692  isexid2  21915  ismndo1  21934  rngo2  21978  rngoueqz  22020  sspval  22224  nmosetre  22267  nmobndseqi  22282  nmobndseqiOLD  22283  orthcom  22612  shsva  22824  shmodsi  22893  h1datomi  23085  nmopsetretALT  23368  nmfnsetre  23382  lnopcnbd  23541  pjclem4  23704  pj3si  23712  ssmd1  23816  atom1d  23858  chjatom  23862  atcvat4i  23902  cdj3lem2a  23941  cdj3lem3a  23944  unitdivcld  24301  xrge0iifiso  24323  dya2iocuni  24635  facgam  24852  deranglem  24854  subfacp1lem6  24873  subfacval2  24875  cvmlift2lem12  25003  relexpsucr  25132  relexpsucl  25134  relexprel  25136  relexpdm  25137  relexprn  25138  relexpadd  25140  relexpindlem  25141  relexpind  25142  rtrclreclem.trans  25148  rtrclreclem.min  25149  dfrtrcl2  25150  rtrclind  25151  dfon2lem6  25417  rdgprc  25424  predpoirr  25474  predfrirr  25475  trpredlem1  25507  wfrlem14  25553  frrlem5e  25592  nodenselem8  25645  axsegconlem1  25858  ax5seglem4  25873  ax5seglem5  25874  axlowdimlem15  25897  axcontlem2  25906  axcontlem4  25908  ifscgr  25980  btwncolinear1  26005  hfelhf  26124  ordcmp  26199  findreccl  26205  nndivlub  26210  opnrebl2  26326  nn0prpw  26328  eqfnun  26425  sdclem2  26448  sdclem1  26449  prdsbnd2  26506  ismtyval  26511  rrnequiv  26546  exidreslem  26554  risci  26605  prtlem11  26717  prtlem15  26726  aovmpt4g  28043  otel3xp  28065  oteqimp  28066  wrdsymb0  28190  swrdvalodm2  28210  swrdvalodm  28211  swrdccatin12lem3  28234  swrdccatin2d  28243  2cshwmod  28279  lswrd0  28283  wlkiswwlk2lem4  28364  el2wlkonot  28389  el2spthonot  28390  frgra3vlem1  28452  3vfriswmgralem  28456  frconngra  28473  frgrawopreglem3  28497  frg2wot1  28508  2spotiundisj  28513  usg2spot2nb  28516  usgreg2spot  28518  bnj168  29159  bnj535  29323  bnj590  29343  bnj594  29345  bnj938  29370  bnj1118  29415  bnj1128  29421  dvelimvNEW7  29524  cvrat4  30302  lcfl6  32360
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 179
  Copyright terms: Public domain W3C validator