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

Theorem syl6ib 218
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 187 . 2  |-  ( ch 
->  th )
41, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3g  261  exp4a  590  mtord  642  exlimd  1820  19.23hOLD  1835  ax12olem6OLD  1982  cbvexd  2064  ax15  2077  2eu3  2344  exists2  2352  necon2bd  2624  necon2d  2625  necon4ad  2636  necon4d  2638  necon1bd  2643  spcimgft  2995  eqsbc3r  3186  reupick  3593  prneimg  3946  invdisj  4169  trin  4280  pwssun  4457  wefrc  4544  ordtri3  4585  suc11  4652  onmindif2  4759  eqbrrdva  5009  elreldm  5061  elres  5148  xp11  5271  ssrnres  5276  opelf  5573  dffo4  5852  dftpos3  6464  swoer  6900  mapsn  7022  domtriord  7220  nneneq  7257  unblem1  7326  supnub  7431  suc11reg  7538  inf3lem2  7548  trcl  7628  en3lplem2  7635  tz9.13  7681  acndom  7896  carduniima  7941  cardinfima  7942  dfac5lem5  7972  fin23lem26  8169  hsmexlem2  8271  axcc4  8283  axdc3lem2  8295  axdclem2  8364  entric  8396  alephval2  8411  cfpwsdom  8423  fpwwe2lem9  8477  ltapr  8886  supsrlem  8950  sup2  9928  nnunb  10181  nneo  10317  indstr  10509  ngtmnft  10719  qsqueeze  10751  qextlt  10753  qextle  10754  icoshft  10983  injresinj  11163  rexuzre  12119  rexico  12120  summo  12474  rpnnen2  12788  divalglem5  12880  ndvdssub  12890  pc2dvds  13215  infpn2  13244  vdwnnlem3  13328  mreiincl  13784  joinlem  14410  meetlem  14417  ablfac1eulem  15593  lbsextlem3  16195  xrsdsreclb  16708  znleval  16798  elcls3  17110  isclo2  17115  tgcn  17278  cnprest  17315  ordthaus  17410  hauscmplem  17431  kgencn2  17550  prdstopn  17621  xkohaus  17646  qtoptop2  17692  filufint  17913  fclsbas  18014  alexsubALTlem3  18041  alexsubALTlem4  18042  ptcmplem2  18045  cldsubg  18101  isucn2  18270  metequiv2  18501  bcthlem5  19242  vieta1  20190  aannenlem2  20207  ulmbdd  20275  angpined  20632  rlimcnp2  20766  amgm  20790  ftalem3  20818  bposlem6  21034  cusgrares  21442  rngosn3  21975  lnon0  22260  ocnel  22761  h1dn0  23015  cnlnssadj  23544  cvnbtwn2  23751  cvnbtwn3  23752  cvnbtwn4  23753  dmdbr2  23767  dmdbr3  23769  dmdbr4  23770  superpos  23818  atcvati  23850  mdsymlem4  23870  sumdmdii  23879  cdj3lem1  23898  elicoelioo  24102  erdszelem9  24846  untangtr  25124  3orel2  25126  dfon2lem6  25366  dfon2lem7  25367  nofv  25533  sltres  25540  nodenselem4  25560  nodenselem7  25563  outsideofrflx  25973  mblfinlem  26151  trer  26217  elicc3  26218  nn0prpw  26224  comppfsc  26285  sdclem1  26345  fdc  26347  incsequz  26350  0rngo  26535  dmncan1  26584  bicomdd  26587  prtlem90  26604  prtlem15  26622  rngunsnply  27254  psgnunilem4  27296  stoweidlem62  27686  atbiffatnnb  27756  2reu3  27841  frgraun  28108  usgreg2spot  28178  ssralv2  28334  truniALT  28345  onfrALTlem3  28349  onfrALTlem2  28351  onfrALTlem1  28353  a9e2ndeq  28365  bnj1280  29107  ax12olem6NEW7  29177  ax15NEW7  29252  cbvexdOLD7  29431  lsatcvat  29545  lfl1  29565  hlrelat2  29897  cvrat  29916  linepsubN  30246  2llnma3r  30282  dihjatcclem4  31916  dochexmidlem1  31955
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