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

Theorem syl6ib 226
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 194 . 2  |-  ( ch 
->  th )
41, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  3imtr3g  269  exp4a  601  mtord  653  exlimd  1845  cbvexd  1973  axc9lem2  1987  equveliOLD  2038  axc14  2060  mo3  2292  2eu3  2360  exists2  2368  necon2bd  2650  necon2d  2651  necon4ad  2662  necon4d  2664  necon1bd  2669  spcimgft  3037  eqsbc3r  3236  reupick  3622  prneimg  4041  invdisj  4269  trin  4383  pwssun  4614  wefrc  4701  ordtri3  4742  suc11  4809  eqbrrdva  4996  elreldm  5051  elres  5133  xp11  5261  ssrnres  5264  opelf  5562  dffo4  5847  onmindif2  6412  dftpos3  6752  swoer  7117  mapsn  7242  domtriord  7445  nneneq  7482  unblem1  7552  supnub  7700  en3lplem2  7809  suc11reg  7813  inf3lem2  7823  trcl  7936  tz9.13  7986  acndom  8209  carduniima  8254  cardinfima  8255  dfac5lem5  8285  fin23lem26  8482  hsmexlem2  8584  axcc4  8596  axdc3lem2  8608  axdclem2  8677  entric  8709  alephval2  8724  cfpwsdom  8736  fpwwe2lem9  8792  ltapr  9201  supsrlem  9265  sup2  10273  nnunb  10562  nneo  10712  indstr  10910  ngtmnft  11126  qsqueeze  11158  qextlt  11160  qextle  11161  icoshft  11393  injresinj  11622  rexuzre  12823  rexico  12824  summo  13177  rpnnen2  13490  divalglem5  13583  ndvdssub  13593  pc2dvds  13927  infpn2  13956  vdwnnlem3  14040  mreiincl  14516  pmtrrn2  15945  psgnunilem4  15982  ablfac1eulem  16546  lbsextlem3  17162  xrsdsreclb  17703  znleval  17828  elcls3  18528  isclo2  18533  tgcn  18697  cnprest  18734  ordthaus  18829  hauscmplem  18850  kgencn2  18971  prdstopn  19042  xkohaus  19067  qtoptop2  19113  filufint  19334  fclsbas  19435  alexsubALTlem3  19462  alexsubALTlem4  19463  ptcmplem2  19466  cldsubg  19522  isucn2  19695  metequiv2  19926  bcthlem5  20680  vieta1  21662  aannenlem2  21679  ulmbdd  21747  angpined  22109  rlimcnp2  22244  amgm  22268  ftalem3  22296  bposlem6  22512  cusgrares  23202  rngosn3  23735  lnon0  24020  ocnel  24523  h1dn0  24777  cnlnssadj  25306  cvnbtwn2  25513  cvnbtwn3  25514  cvnbtwn4  25515  dmdbr2  25529  dmdbr3  25531  dmdbr4  25532  superpos  25580  atcvati  25612  mdsymlem4  25632  sumdmdii  25641  cdj3lem1  25660  mul2lt0bi  25866  elicoelioo  25890  archiabl  26038  erdszelem9  26934  untangtr  27211  3orel2  27213  dfon2lem6  27447  dfon2lem7  27448  nofv  27644  sltres  27651  nodenselem4  27671  nodenselem7  27674  outsideofrflx  28004  mblfinlem2  28270  trer  28352  elicc3  28353  nn0prpw  28359  comppfsc  28420  sdclem1  28480  fdc  28482  incsequz  28485  0rngo  28668  dmncan1  28717  exlimddvf  28770  bicomdd  28829  prtlem90  28844  prtlem15  28862  rngunsnply  29372  stoweidlem62  29700  atbiffatnnb  29770  2reu3  29855  frgraun  30431  usgreg2spot  30503  ssralv2  30934  truniALT  30946  onfrALTlem3  30950  onfrALTlem2  30952  onfrALTlem1  30954  ax6e2ndeq  30966  bnj1280  31710  bj-cbvexdv  31865  lsatcvat  32265  lfl1  32285  hlrelat2  32617  cvrat  32636  linepsubN  32966  2llnma3r  33002  dihjatcclem4  34636  dochexmidlem1  34675
  Copyright terms: Public domain W3C validator