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  19.23v  1761  exlimd  1915  cbvexd  2027  axc9lem2  2041  equveliOLD  2090  axc14  2114  mo3  2324  2eu3  2379  2eu6  2383  exists2  2389  necon2bd  2672  necon1bdOLD  2676  necon4adOLD  2678  necon2d  2683  necon4d  2684  spcimgft  3185  eqsbc3r  3389  reupick  3789  prneimg  4213  invdisj  4445  trin  4560  pwssun  4795  wefrc  4882  ordtri3  4923  suc11  4990  eqbrrdva  5182  elreldm  5237  elres  5319  xp11  5449  ssrnres  5452  opelf  5753  dffo4  6048  onmindif2  6646  dftpos3  6991  swoer  7357  mapsn  7479  domtriord  7682  nneneq  7719  unblem1  7790  supnub  7939  en3lplem2  8049  suc11reg  8053  inf3lem2  8063  trcl  8176  tz9.13  8226  acndom  8449  carduniima  8494  cardinfima  8495  dfac5lem5  8525  fin23lem26  8722  hsmexlem2  8824  axcc4  8836  axdc3lem2  8848  axdclem2  8917  entric  8949  alephval2  8964  cfpwsdom  8976  fpwwe2lem9  9033  ltapr  9440  supsrlem  9505  sup2  10519  nnunb  10812  nneo  10967  indstr  11175  ngtmnft  11393  qsqueeze  11425  qextlt  11427  qextle  11428  icoshft  11667  injresinj  11929  rexuzre  13197  rexico  13198  summo  13551  rpnnen2  13971  divalglem5  14067  ndvdssub  14077  pc2dvds  14414  infpn2  14443  vdwnnlem3  14527  mreiincl  15013  intopsn  16009  pmtrrn2  16612  psgnunilem4  16649  ablfac1eulem  17250  lbsextlem3  17933  xrsdsreclb  18592  znleval  18720  elcls3  19711  isclo2  19716  tgcn  19880  cnprest  19917  ordthaus  20012  hauscmplem  20033  comppfsc  20159  kgencn2  20184  prdstopn  20255  xkohaus  20280  qtoptop2  20326  tgqtop  20339  filufint  20547  fclsbas  20648  alexsubALTlem3  20675  alexsubALTlem4  20676  ptcmplem2  20679  cldsubg  20735  isucn2  20908  metequiv2  21139  bcthlem5  21893  vieta1  22834  aannenlem2  22851  ulmbdd  22919  angpined  23287  rlimcnp2  23422  amgm  23446  ftalem3  23474  bposlem6  23690  cusgrares  24599  frgraun  25123  usgreg2spot  25194  rngosn3  25555  lnon0  25840  ocnel  26343  h1dn0  26597  cnlnssadj  27126  cvnbtwn2  27333  cvnbtwn3  27334  cvnbtwn4  27335  dmdbr2  27349  dmdbr3  27351  dmdbr4  27352  superpos  27400  atcvati  27432  mdsymlem4  27452  sumdmdii  27461  cdj3lem1  27480  mul2lt0bi  27726  elicoelioo  27749  archiabl  27902  erdszelem9  28840  untangtr  29283  3orel2  29285  dfon2lem6  29416  dfon2lem7  29417  nofv  29613  sltres  29620  nodenselem4  29640  nodenselem7  29643  outsideofrflx  29961  wl-mo3t  30205  mblfinlem2  30236  trer  30318  elicc3  30319  nn0prpw  30325  sdclem1  30420  fdc  30422  incsequz  30425  0rngo  30608  dmncan1  30657  bicomdd  30767  prtlem90  30782  prtlem15  30800  rngunsnply  31305  isprm7  31375  stoweidlem62  32026  atbiffatnnb  32290  2reu3  32375  copisnmnd  32738  ssralv2  33423  truniALT  33434  onfrALTlem3  33438  onfrALTlem2  33440  onfrALTlem1  33442  ax6e2ndeq  33454  bnj1280  34198  bj-cbvexdv  34423  lsatcvat  34897  lfl1  34917  hlrelat2  35249  cvrat  35268  linepsubN  35598  2llnma3r  35634  dihjatcclem4  37270  dochexmidlem1  37309
  Copyright terms: Public domain W3C validator