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

Theorem syl6ib 229
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-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 197 . 2  |-  ( ch 
->  th )
41, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr3g  272  exp4a  609  mtord  664  19.23v  1810  exlimd  1972  cbvexd  2082  axc9lem2  2096  axc14  2167  mo3  2306  2eu3  2357  2eu6  2361  exists2  2367  necon2bd  2646  necon1bdOLD  2650  necon4adOLD  2652  necon2d  2657  necon4d  2658  spcimgft  3163  eqsbc3r  3362  reupick  3763  prneimg  4184  invdisj  4415  trin  4530  pwssun  4760  wefrc  4848  eqbrrdva  5024  elreldm  5079  elres  5160  xp11  5292  ssrnres  5295  ordtri3  5478  suc11  5545  opelf  5762  dffo4  6053  onmindif2  6653  dftpos3  6999  swoer  7399  mapsn  7521  domtriord  7724  nneneq  7761  unblem1  7829  supnub  7982  infnlb  8014  en3lplem2  8120  suc11reg  8124  inf3lem2  8134  trcl  8211  tz9.13  8261  acndom  8480  carduniima  8525  cardinfima  8526  dfac5lem5  8556  fin23lem26  8753  hsmexlem2  8855  axcc4  8867  axdc3lem2  8879  axdclem2  8948  entric  8980  alephval2  8995  cfpwsdom  9007  fpwwe2lem9  9062  ltapr  9469  supsrlem  9534  sup2  10565  nnunb  10865  nneo  11019  indstr  11227  mul2lt0bi  11402  ngtmnft  11462  qsqueeze  11494  qextlt  11496  qextle  11497  icoshft  11752  injresinj  12022  rexuzre  13394  rexico  13395  summo  13761  rpnnen2  14256  divalglem5  14353  ndvdssub  14363  pc2dvds  14791  infpn2  14820  vdwnnlem3  14910  mreiincl  15453  intopsn  16449  pmtrrn2  17052  psgnunilem4  17089  ablfac1eulem  17640  lbsextlem3  18318  xrsdsreclb  18950  znleval  19056  elcls3  20030  isclo2  20035  tgcn  20199  cnprest  20236  ordthaus  20331  hauscmplem  20352  comppfsc  20478  kgencn2  20503  prdstopn  20574  xkohaus  20599  qtoptop2  20645  tgqtop  20658  filufint  20866  fclsbas  20967  alexsubALTlem3  20995  alexsubALTlem4  20996  ptcmplem2  20999  cldsubg  21056  isucn2  21225  metequiv2  21456  bcthlem5  22189  vieta1  23133  aannenlem2  23150  ulmbdd  23218  angpined  23621  rlimcnp2  23757  amgm  23781  ftalem3  23864  bposlem6  24080  cusgrares  25045  frgraun  25569  usgreg2spot  25640  rngosn3  25999  lnon0  26284  ocnel  26786  h1dn0  27040  cnlnssadj  27568  cvnbtwn2  27775  cvnbtwn3  27776  cvnbtwn4  27777  dmdbr2  27791  dmdbr3  27793  dmdbr4  27794  superpos  27842  atcvati  27874  mdsymlem4  27894  sumdmdii  27903  cdj3lem1  27922  elicoelioo  28196  archiabl  28353  bnj1280  29617  erdszelem9  29710  untangtr  30129  3orel2  30131  dfon2lem6  30221  dfon2lem7  30222  nofv  30331  sltres  30338  nodenselem4  30358  nodenselem7  30361  outsideofrflx  30679  trer  30757  elicc3  30758  nn0prpw  30764  bj-cbvexdv  31081  topdifinffinlem  31484  icorempt2  31488  isbasisrelowllem1  31492  relowlpssretop  31501  wl-mo3t  31609  poimirlem23  31667  poimirlem29  31673  poimirlem32  31676  poimir  31677  mblfinlem2  31682  sdclem1  31776  fdc  31778  incsequz  31781  0rngo  31964  dmncan1  32013  bicomdd  32122  prtlem90  32137  prtlem15  32155  lsatcvat  32325  lfl1  32345  hlrelat2  32677  cvrat  32696  linepsubN  33026  2llnma3r  33062  dihjatcclem4  34698  dochexmidlem1  34737  rngunsnply  35738  frege124d  35992  frege77  36173  frege116  36212  isprm7  36297  ssralv2  36525  truniALT  36539  onfrALTlem3  36547  onfrALTlem2  36549  onfrALTlem1  36551  ax6e2ndeq  36563  stoweidlem62  37492  stoweidlem62OLD  37493  atbiffatnnb  37900  2reu3  38000  gboge7  38254  gbege6  38256  copisnmnd  38567
  Copyright terms: Public domain W3C validator