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  1811  exlimd  1974  cbvexd  2086  axc9lem2  2100  axc9lem2OLD  2101  axc14  2172  mo3  2308  2eu3  2356  2eu6  2359  exists2  2363  necon2bd  2612  necon2d  2619  necon4d  2620  spcimgft  3095  eqsbc3r  3294  reupick  3695  prneimg  4119  invdisj  4350  trin  4466  pwssun  4697  wefrc  4785  eqbrrdva  4961  elreldm  5016  elres  5097  xp11  5229  ssrnres  5232  ordtri3  5416  suc11  5483  opelf  5700  dffo4  5992  onmindif2  6592  dftpos3  6941  swoer  7341  mapsn  7463  domtriord  7666  nneneq  7703  unblem1  7771  supnub  7924  infnlb  7956  en3lplem2  8068  suc11reg  8072  inf3lem2  8082  trcl  8159  tz9.13  8209  acndom  8428  carduniima  8473  cardinfima  8474  dfac5lem5  8504  fin23lem26  8701  hsmexlem2  8803  axcc4  8815  axdc3lem2  8827  axdclem2  8896  entric  8928  alephval2  8943  cfpwsdom  8955  fpwwe2lem9  9009  ltapr  9416  supsrlem  9481  sup2  10511  nnunb  10811  nneo  10965  indstr  11173  mul2lt0bi  11348  ngtmnft  11408  qsqueeze  11440  qextlt  11442  qextle  11443  icoshft  11700  injresinj  11970  rexuzre  13354  rexico  13355  summo  13721  rpnnen2  14216  divalglem5OLD  14314  divalglem5  14315  ndvdssub  14326  pc2dvds  14766  infpn2  14795  vdwnnlem3  14885  mreiincl  15440  intopsn  16436  pmtrrn2  17039  psgnunilem4  17076  ablfac1eulem  17643  lbsextlem3  18321  xrsdsreclb  18953  znleval  19062  elcls3  20036  isclo2  20041  tgcn  20205  cnprest  20242  ordthaus  20337  hauscmplem  20358  comppfsc  20484  kgencn2  20509  prdstopn  20580  xkohaus  20605  qtoptop2  20651  tgqtop  20664  filufint  20872  fclsbas  20973  alexsubALTlem3  21001  alexsubALTlem4  21002  ptcmplem2  21005  cldsubg  21062  isucn2  21231  metequiv2  21462  bcthlem5  22233  vieta1  23202  aannenlem2  23222  ulmbdd  23290  angpined  23693  rlimcnp2  23829  amgm  23853  ftalem3  23936  bposlem6  24154  cusgrares  25137  frgraun  25661  usgreg2spot  25732  rngosn3  26091  lnon0  26376  ocnel  26888  h1dn0  27142  cnlnssadj  27670  cvnbtwn2  27877  cvnbtwn3  27878  cvnbtwn4  27879  dmdbr2  27893  dmdbr3  27895  dmdbr4  27896  superpos  27944  atcvati  27976  mdsymlem4  27996  sumdmdii  28005  cdj3lem1  28024  elicoelioo  28305  archiabl  28461  bnj1280  29776  erdszelem9  29869  untangtr  30288  3orel2  30290  dfon2lem6  30380  dfon2lem7  30381  nofv  30490  sltres  30497  nodenselem4  30517  nodenselem7  30520  outsideofrflx  30838  trer  30916  elicc3  30917  nn0prpw  30923  bj-cbvexdv  31242  bj-spcimdv  31404  topdifinffinlem  31657  icorempt2  31661  isbasisrelowllem1  31665  relowlpssretop  31674  wl-mo3t  31812  poimirlem23  31870  poimirlem29  31876  poimirlem32  31879  poimir  31880  mblfinlem2  31885  sdclem1  31979  fdc  31981  incsequz  31984  0rngo  32167  dmncan1  32216  bicomdd  32325  prtlem90  32340  prtlem15  32358  lsatcvat  32528  lfl1  32548  hlrelat2  32880  cvrat  32899  linepsubN  33229  2llnma3r  33265  dihjatcclem4  34901  dochexmidlem1  34940  rngunsnply  35952  mptrcllem  36133  frege124d  36266  frege77  36449  frege116  36488  isprm7  36573  ssralv2  36801  truniALT  36815  onfrALTlem3  36823  onfrALTlem2  36825  onfrALTlem1  36827  ax6e2ndeq  36839  stoweidlem62  37806  stoweidlem62OLD  37807  atbiffatnnb  38314  2reu3  38423  gboge7  38677  gbege6  38679  upgredg  38990  copisnmnd  39400
  Copyright terms: Public domain W3C validator