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  2059  ax15  2070  2eu3  2336  exists2  2344  necon2bd  2616  necon2d  2617  necon4ad  2628  necon4d  2630  necon1bd  2635  spcimgft  2987  eqsbc3r  3178  reupick  3585  prneimg  3938  invdisj  4161  trin  4272  pwssun  4449  wefrc  4536  ordtri3  4577  suc11  4644  onmindif2  4751  eqbrrdva  5001  elreldm  5053  elres  5140  xp11  5263  ssrnres  5268  opelf  5565  dffo4  5844  dftpos3  6456  swoer  6892  mapsn  7014  domtriord  7212  nneneq  7249  unblem1  7318  supnub  7423  suc11reg  7530  inf3lem2  7540  trcl  7620  en3lplem2  7627  tz9.13  7673  acndom  7888  carduniima  7933  cardinfima  7934  dfac5lem5  7964  fin23lem26  8161  hsmexlem2  8263  axcc4  8275  axdc3lem2  8287  axdclem2  8356  entric  8388  alephval2  8403  cfpwsdom  8415  fpwwe2lem9  8469  ltapr  8878  supsrlem  8942  sup2  9920  nnunb  10173  nneo  10309  indstr  10501  ngtmnft  10711  qsqueeze  10743  qextlt  10745  qextle  10746  icoshft  10975  injresinj  11155  rexuzre  12111  rexico  12112  summo  12466  rpnnen2  12780  divalglem5  12872  ndvdssub  12882  pc2dvds  13207  infpn2  13236  vdwnnlem3  13320  mreiincl  13776  joinlem  14402  meetlem  14409  ablfac1eulem  15585  lbsextlem3  16187  xrsdsreclb  16700  znleval  16790  elcls3  17102  isclo2  17107  tgcn  17270  cnprest  17307  ordthaus  17402  hauscmplem  17423  kgencn2  17542  prdstopn  17613  xkohaus  17638  qtoptop2  17684  filufint  17905  fclsbas  18006  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  cldsubg  18093  isucn2  18262  metequiv2  18493  bcthlem5  19234  vieta1  20182  aannenlem2  20199  ulmbdd  20267  angpined  20624  rlimcnp2  20758  amgm  20782  ftalem3  20810  bposlem6  21026  cusgrares  21434  rngosn3  21967  lnon0  22252  ocnel  22753  h1dn0  23007  cnlnssadj  23536  cvnbtwn2  23743  cvnbtwn3  23744  cvnbtwn4  23745  dmdbr2  23759  dmdbr3  23761  dmdbr4  23762  superpos  23810  atcvati  23842  mdsymlem4  23862  sumdmdii  23871  cdj3lem1  23890  elicoelioo  24094  erdszelem9  24838  untangtr  25116  3orel2  25118  dfon2lem6  25358  dfon2lem7  25359  nofv  25525  sltres  25532  nodenselem4  25552  nodenselem7  25555  outsideofrflx  25965  mblfinlem  26143  trer  26209  elicc3  26210  nn0prpw  26216  comppfsc  26277  sdclem1  26337  fdc  26339  incsequz  26342  0rngo  26527  dmncan1  26576  bicomdd  26579  prtlem90  26596  prtlem15  26614  rngunsnply  27246  psgnunilem4  27288  stoweidlem62  27678  atbiffatnnb  27748  2reu3  27833  frgraun  28100  usgreg2spot  28170  ssralv2  28326  truniALT  28337  onfrALTlem3  28341  onfrALTlem2  28343  onfrALTlem1  28345  a9e2ndeq  28357  bnj1280  29095  ax12olem6NEW7  29165  ax15NEW7  29240  cbvexdOLD7  29419  lsatcvat  29533  lfl1  29553  hlrelat2  29885  cvrat  29904  linepsubN  30234  2llnma3r  30270  dihjatcclem4  31904  dochexmidlem1  31943
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