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

Theorem syl5ib 212
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ib  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32biimpd 200 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3syl5 31 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl5ibcom  213  syl5ibr  214  19.23tOLD  1839  dvelimdf  2071  sbft  2117  nfsb4tOLD  2130  ax11indalem  2276  ax11inda2ALT  2277  gencl  2986  spsbc  3175  eqsbc3r  3220  ssnelpss  3693  uniintsn  4089  prex  4408  ordtri3  4619  ssonprc  4774  posn  4948  optocl  4954  xpexr  5309  relcnvexb  5409  funimass1  5528  dmfex  5628  f1ocnvb  5690  eqfnfv2  5830  elpreima  5852  fconst5  5951  dff13  6006  f1ocnvfv  6018  f1ocnvfvb  6019  fliftfun  6036  frxp  6458  mpt2xopn0yelv  6466  rntpos  6494  sorpsscmpl  6535  eusvobj2  6584  oawordeulem  6799  oalimcl  6805  odi  6824  omeulem2  6828  oeeulem  6846  erexb  6932  unxpdomlem2  7316  dif1enOLD  7342  dif1en  7343  enp1ilem  7344  findcard2  7350  isfinite2  7367  unfi  7376  fodomfib  7388  inf0  7578  rankxplim2  7806  scott0  7812  ficardom  7850  cardaleph  7972  dfac5  8011  cflim2  8145  fin23lem23  8208  fin23lem28  8222  isf32lem5  8239  domtriomlem  8324  ac6num  8361  zorn2lem5  8382  zorn2lem6  8383  iunfo  8416  axrepndlem2  8470  axregnd  8481  hargch  8554  addcanpi  8778  mulcanpi  8779  indpi  8786  ltaddnq  8853  ltexnq  8854  prlem934  8912  ltaddpr2  8914  ltaprlem  8923  supsrlem  8988  ssxr  9147  ltxrlt  9148  addcan  9252  addcan2  9253  neg11  9354  negreb  9368  mulcand  9657  receu  9669  lemul1a  9866  cju  9998  nn1suc  10023  nnaddcl  10024  nndivtr  10043  znegclb  10316  zmulcl  10326  zeo  10357  uz11  10510  uzp1  10521  eqreznegel  10563  rpnnen1  10607  xrltne  10755  xneg11  10803  xnegdi  10829  xrsupss  10889  xrinfmss  10890  elfznelfzob  11195  modadd1  11280  modmul1  11281  om2uzlti  11292  bccmpl  11602  hashen  11633  fz1eqb  11639  hashfn  11651  hashnn0n0nn  11666  hashtpg  11693  ccatopth  11778  ccatopth2  11779  cj11  11969  rennim  12046  cnpart  12047  sqrmo  12059  sqrgt0  12066  sqreulem  12165  sqreu  12166  lo1o1  12328  lo1eq  12364  rlimeq  12365  sumss  12520  cvgcmp  12597  efne0  12700  dvdseq  12899  divalglem8  12922  bitsinv1lem  12955  pcfac  13270  prmreclem3  13288  sectmon  14005  yoniso  14384  lubid  14441  oduposb  14565  grpinveu  14841  mulgass  14922  galcan  15083  cayleylem2  15113  odbezout  15196  odeq1  15198  dvreq1  15800  unitrrg  16355  coe1tm  16667  frgpcyg  16856  obslbs  16959  tgss3  17053  uptx  17659  txindislem  17667  qtopeu  17750  hmeocnvb  17808  qtophmeo  17851  trufil  17944  ufinffr  17963  ghmcnp  18146  tgioo  18829  lmmcvg  19216  bcth3  19286  ovolunlem1a  19394  vitali  19507  ismbf  19524  ismbfcn  19525  rolle  19876  itgsubstlem  19934  vieta1lem2  20230  elqaalem3  20240  aacjcl  20246  efif1olem4  20449  lognegb  20486  logcj  20503  argimgt0  20509  logdmnrp  20534  logcnlem3  20537  logrec  20663  dcubic  20688  isppw  20899  rplogsumlem2  21181  pntpbnd1  21282  is2wlk  21567  grpoinveu  21812  grpoinvf  21830  diporthcom  22217  norm1exi  22754  shmodsi  22893  shmodi  22894  dfch2  22911  orthin  22950  chssoc  23000  spansncvi  23156  kbpj  23461  lnopunilem1  23515  cnlnssadj  23585  bra11  23613  strlem4  23759  strlem5  23760  hstrlem4  23767  hstrlem5  23768  dmdmd  23805  mdslle1i  23822  mdslle2i  23823  mdslmd1lem1  23830  atcvatlem  23890  atcvat4i  23902  mdsymlem3  23910  bcm1n  24153  xmulcand  24169  xreceu  24170  tpr2rico  24312  fprodser  25277  funpsstri  25391  sltres  25621  nofulllem1  25659  nofulllem2  25660  axlowdimlem16  25898  btwnintr  25955  idinside  26020  btwnconn1lem13  26035  fneval  26369  ismtybndlem  26517  grpoeqdivid  26558  0rngo  26639  expgrowth  27531  sbiota1  27613  xpexcnv  27637  wrdeq0  28174  wrdlenge2n0  28178  swrdccatin2  28212  swrdccat3a  28219  swrdccatin1d  28222  usgra2pth  28313  el2wlkonot  28338  frg2wot1  28448  bnj1125  29363  nfsb4twAUX7  29578  nfsb4tOLD7  29747  nfsb4tw2AUXOLD7  29748  lcvexchlem4  29837  lcvexchlem5  29838  opcon3b  29996  2dim  30269  ps-1  30276  paddclN  30641  ltrnnid  30935  cdleme22b  31140  dihmeetlem13N  32119  dih1dimatlem  32129  dihlspsnat  32133
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