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

Theorem syl6ib 217
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ib.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6ib.2  |-  ( ch  <->  th )
Assertion
Ref Expression
syl6ib  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6ib
StepHypRef Expression
1 syl6ib.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ib.2 . . 3  |-  ( ch  <->  th )
32biimpi 186 . 2  |-  ( ch 
->  th )
41, 3syl6 29 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3g  260  exp4a  589  mtord  641  exlimdv  1664  19.23h  1728  ax12olem6  1873  cbvexd  1949  ax15  1961  2eu3  2225  exists2  2233  necon2bd  2495  necon2d  2496  necon4ad  2507  necon4d  2509  necon1bd  2514  spcimgft  2859  eqsbc3r  3048  reupick  3452  invdisj  4012  trin  4123  pwssun  4299  wefrc  4387  ordtri3  4428  suc11  4496  onmindif2  4603  elreldm  4903  elres  4990  xp11  5111  ssrnres  5116  opelf  5404  dffo4  5676  dftpos3  6252  swoer  6688  mapsn  6809  domtriord  7007  nneneq  7044  unblem1  7109  supnub  7213  suc11reg  7320  inf3lem2  7330  trcl  7410  en3lplem2  7417  tz9.13  7463  acndom  7678  carduniima  7723  cardinfima  7724  dfac5lem5  7754  fin23lem26  7951  hsmexlem2  8053  axcc4  8065  axdc3lem2  8077  axdclem2  8147  entric  8179  alephval2  8194  cfpwsdom  8206  fpwwe2lem9  8260  ltapr  8669  supsrlem  8733  sup2  9710  nnunb  9961  nneo  10095  indstr  10287  ngtmnft  10496  qsqueeze  10528  qextlt  10530  qextle  10531  icoshft  10758  rexuzre  11836  rexico  11837  summo  12190  rpnnen2  12504  divalglem5  12596  ndvdssub  12606  pc2dvds  12931  infpn2  12960  vdwnnlem3  13044  mreiincl  13498  joinlem  14124  meetlem  14131  ablfac1eulem  15307  lbsextlem3  15913  xrsdsreclb  16418  znleval  16508  elcls3  16820  isclo2  16825  tgcn  16982  cnprest  17017  ordthaus  17112  hauscmplem  17133  kgencn2  17252  prdstopn  17322  xkohaus  17347  qtoptop2  17390  filufint  17615  fclsbas  17716  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  cldsubg  17793  metequiv2  18056  bcthlem5  18750  vieta1  19692  aannenlem2  19709  ulmbdd  19775  angpined  20127  rlimcnp2  20261  amgm  20285  ftalem3  20312  bposlem6  20528  rngosn3  21093  lnon0  21376  ocnel  21877  h1dn0  22131  cnlnssadj  22660  cvnbtwn2  22867  cvnbtwn3  22868  cvnbtwn4  22869  dmdbr2  22883  dmdbr3  22885  dmdbr4  22886  superpos  22934  atcvati  22966  mdsymlem4  22986  sumdmdii  22995  cdj3lem1  23014  elicoelioo  23271  erdszelem9  23730  untangtr  24060  3orel2  24062  dfon2lem6  24144  dfon2lem7  24145  nofv  24311  sltres  24318  nodenselem4  24338  nodenselem7  24341  outsideofrflx  24750  oprabex2gpop  25036  islatalg  25183  iintlem1  25610  trer  26227  elicc3  26228  nn0prpw  26239  comppfsc  26307  sdclem1  26453  fdc  26455  incsequz  26458  0rngo  26652  dmncan1  26701  bicomdd  26705  prtlem90  26723  prtlem15  26743  rngunsnply  27378  psgnunilem4  27420  stoweidlem62  27811  2reu3  27966  prneimg  28073  ssralv2  28294  truniALT  28305  onfrALTlem3  28309  onfrALTlem2  28311  onfrALTlem1  28313  a9e2ndeq  28325  bnj1280  29050  a12study2  29134  a12study10  29136  a12study10n  29137  lsatcvat  29240  lfl1  29260  hlrelat2  29592  cvrat  29611  linepsubN  29941  2llnma3r  29977  dihjatcclem4  31611  dochexmidlem1  31650
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