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, 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 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  606  mtord  660  exlimd  1861  19.23v  1932  cbvexd  1999  axc9lem2  2013  equveliOLD  2062  axc14  2086  mo3  2320  2eu3  2389  2eu6  2393  exists2  2399  necon2bd  2682  necon1bdOLD  2686  necon4adOLD  2688  necon2d  2693  necon4d  2694  spcimgft  3189  eqsbc3r  3393  reupick  3782  prneimg  4207  invdisj  4436  trin  4550  pwssun  4786  wefrc  4873  ordtri3  4914  suc11  4981  eqbrrdva  5172  elreldm  5227  elres  5309  xp11  5442  ssrnres  5445  opelf  5747  dffo4  6037  onmindif2  6631  dftpos3  6973  swoer  7339  mapsn  7460  domtriord  7663  nneneq  7700  unblem1  7772  supnub  7922  en3lplem2  8032  suc11reg  8036  inf3lem2  8046  trcl  8159  tz9.13  8209  acndom  8432  carduniima  8477  cardinfima  8478  dfac5lem5  8508  fin23lem26  8705  hsmexlem2  8807  axcc4  8819  axdc3lem2  8831  axdclem2  8900  entric  8932  alephval2  8947  cfpwsdom  8959  fpwwe2lem9  9016  ltapr  9423  supsrlem  9488  sup2  10499  nnunb  10791  nneo  10944  indstr  11150  ngtmnft  11368  qsqueeze  11400  qextlt  11402  qextle  11403  icoshft  11642  injresinj  11894  rexuzre  13148  rexico  13149  summo  13502  rpnnen2  13820  divalglem5  13914  ndvdssub  13924  pc2dvds  14261  infpn2  14290  vdwnnlem3  14374  mreiincl  14851  intopsn  15782  pmtrrn2  16291  psgnunilem4  16328  ablfac1eulem  16925  lbsextlem3  17606  xrsdsreclb  18261  znleval  18388  elcls3  19378  isclo2  19383  tgcn  19547  cnprest  19584  ordthaus  19679  hauscmplem  19700  kgencn2  19821  prdstopn  19892  xkohaus  19917  qtoptop2  19963  filufint  20184  fclsbas  20285  alexsubALTlem3  20312  alexsubALTlem4  20313  ptcmplem2  20316  cldsubg  20372  isucn2  20545  metequiv2  20776  bcthlem5  21530  vieta1  22470  aannenlem2  22487  ulmbdd  22555  angpined  22917  rlimcnp2  23052  amgm  23076  ftalem3  23104  bposlem6  23320  cusgrares  24176  frgraun  24700  usgreg2spot  24772  rngosn3  25132  lnon0  25417  ocnel  25920  h1dn0  26174  cnlnssadj  26703  cvnbtwn2  26910  cvnbtwn3  26911  cvnbtwn4  26912  dmdbr2  26926  dmdbr3  26928  dmdbr4  26929  superpos  26977  atcvati  27009  mdsymlem4  27029  sumdmdii  27038  cdj3lem1  27057  mul2lt0bi  27265  elicoelioo  27285  archiabl  27432  erdszelem9  28311  untangtr  28589  3orel2  28591  dfon2lem6  28825  dfon2lem7  28826  nofv  29022  sltres  29029  nodenselem4  29049  nodenselem7  29052  outsideofrflx  29382  wl-mo3t  29626  mblfinlem2  29657  trer  29739  elicc3  29740  nn0prpw  29746  comppfsc  29807  sdclem1  29867  fdc  29869  incsequz  29872  0rngo  30055  dmncan1  30104  exlimddvf  30157  bicomdd  30215  prtlem90  30230  prtlem15  30248  rngunsnply  30755  isprm7  30823  stoweidlem62  31390  atbiffatnnb  31603  2reu3  31688  ssralv2  32398  truniALT  32410  onfrALTlem3  32414  onfrALTlem2  32416  onfrALTlem1  32418  ax6e2ndeq  32430  bnj1280  33173  bj-cbvexdv  33401  lsatcvat  33865  lfl1  33885  hlrelat2  34217  cvrat  34236  linepsubN  34566  2llnma3r  34602  dihjatcclem4  36236  dochexmidlem1  36275
  Copyright terms: Public domain W3C validator