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

Theorem syl6ib 234
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 199 . 2  |-  ( ch 
->  th )
41, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3imtr3g  277  exp4a  615  mtord  670  19.23v  1828  exlimd  2007  cbvexd  2129  axc9lem2  2143  axc9lem2OLD  2144  axc14  2211  mo3  2346  2eu3  2394  2eu6  2397  exists2  2401  necon2bd  2651  necon2d  2658  necon4d  2659  spcimgft  3136  eqsbc3r  3335  reupick  3738  prneimg  4169  invdisj  4404  trin  4520  pwssun  4758  wefrc  4846  eqbrrdva  5022  elreldm  5077  elres  5158  xp11  5290  ssrnres  5293  ordtri3  5477  suc11  5544  opelf  5767  dffo4  6060  onmindif2  6665  dftpos3  7016  swoer  7416  mapsn  7538  domtriord  7743  nneneq  7780  unblem1  7848  supnub  8001  infnlb  8033  en3lplem2  8145  suc11reg  8149  inf3lem2  8159  trcl  8237  tz9.13  8287  acndom  8507  carduniima  8552  cardinfima  8553  dfac5lem5  8583  fin23lem26  8780  hsmexlem2  8882  axcc4  8894  axdc3lem2  8906  axdclem2  8975  entric  9007  alephval2  9022  cfpwsdom  9034  fpwwe2lem9  9088  ltapr  9495  supsrlem  9560  sup2  10592  nnunb  10893  nneo  11047  indstr  11255  mul2lt0bi  11430  ngtmnft  11490  qsqueeze  11522  qextlt  11524  qextle  11525  icoshft  11782  injresinj  12056  rexuzre  13463  rexico  13464  summo  13831  rpnnen2  14326  divalglem5OLD  14424  divalglem5  14425  ndvdssub  14436  pc2dvds  14876  infpn2  14905  vdwnnlem3  14995  mreiincl  15550  intopsn  16546  pmtrrn2  17149  psgnunilem4  17186  ablfac1eulem  17753  lbsextlem3  18431  xrsdsreclb  19063  znleval  19173  elcls3  20147  isclo2  20152  tgcn  20316  cnprest  20353  ordthaus  20448  hauscmplem  20469  comppfsc  20595  kgencn2  20620  prdstopn  20691  xkohaus  20716  qtoptop2  20762  tgqtop  20775  filufint  20983  fclsbas  21084  alexsubALTlem3  21112  alexsubALTlem4  21113  ptcmplem2  21116  cldsubg  21173  isucn2  21342  metequiv2  21573  bcthlem5  22344  vieta1  23313  aannenlem2  23333  ulmbdd  23401  angpined  23804  rlimcnp2  23940  amgm  23964  ftalem3  24047  bposlem6  24265  cusgrares  25248  frgraun  25772  usgreg2spot  25843  rngosn3  26202  lnon0  26487  ocnel  26999  h1dn0  27253  cnlnssadj  27781  cvnbtwn2  27988  cvnbtwn3  27989  cvnbtwn4  27990  dmdbr2  28004  dmdbr3  28006  dmdbr4  28007  superpos  28055  atcvati  28087  mdsymlem4  28107  sumdmdii  28116  cdj3lem1  28135  elicoelioo  28408  archiabl  28563  bnj1280  29877  erdszelem9  29970  untangtr  30389  3orel2  30391  dfon2lem6  30482  dfon2lem7  30483  nofv  30592  sltres  30599  nodenselem4  30621  nodenselem7  30624  outsideofrflx  30942  trer  31020  elicc3  31021  nn0prpw  31027  bj-cbvexdv  31381  bj-spcimdv  31537  topdifinffinlem  31794  icorempt2  31798  isbasisrelowllem1  31802  relowlpssretop  31811  wl-mo3t  31949  poimirlem23  32007  poimirlem29  32013  poimirlem32  32016  poimir  32017  mblfinlem2  32022  sdclem1  32116  fdc  32118  incsequz  32121  0rngo  32304  dmncan1  32353  bicomdd  32462  prtlem90  32475  prtlem15  32491  lsatcvat  32660  lfl1  32680  hlrelat2  33012  cvrat  33031  linepsubN  33361  2llnma3r  33397  dihjatcclem4  35033  dochexmidlem1  35072  rngunsnply  36083  mptrcllem  36264  frege124d  36397  frege77  36580  frege116  36619  isprm7  36703  ssralv2  36931  truniALT  36945  onfrALTlem3  36953  onfrALTlem2  36955  onfrALTlem1  36957  ax6e2ndeq  36969  stoweidlem62  37960  stoweidlem62OLD  37961  atbiffatnnb  38537  2reu3  38646  gboge7  38901  gbege6  38903  upgredg  39275  uhgrvd00  39620  pthdlem2lem  39792  copisnmnd  40081
  Copyright terms: Public domain W3C validator