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

Theorem syl6ib 218
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-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 187 . 2  |-  ( ch 
->  th )
41, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3g  261  exp4a  590  mtord  642  exlimd  1824  19.23hOLD  1839  cbvexd  1988  ax12olem6OLD  2016  ax15  2107  2eu3  2363  exists2  2371  necon2bd  2653  necon2d  2654  necon4ad  2665  necon4d  2667  necon1bd  2672  spcimgft  3027  eqsbc3r  3218  reupick  3625  prneimg  3978  invdisj  4201  trin  4312  pwssun  4489  wefrc  4576  ordtri3  4617  suc11  4685  onmindif2  4792  eqbrrdva  5042  elreldm  5094  elres  5181  xp11  5304  ssrnres  5309  opelf  5606  dffo4  5885  dftpos3  6497  swoer  6933  mapsn  7055  domtriord  7253  nneneq  7290  unblem1  7359  supnub  7467  suc11reg  7574  inf3lem2  7584  trcl  7664  en3lplem2  7671  tz9.13  7717  acndom  7932  carduniima  7977  cardinfima  7978  dfac5lem5  8008  fin23lem26  8205  hsmexlem2  8307  axcc4  8319  axdc3lem2  8331  axdclem2  8400  entric  8432  alephval2  8447  cfpwsdom  8459  fpwwe2lem9  8513  ltapr  8922  supsrlem  8986  sup2  9964  nnunb  10217  nneo  10353  indstr  10545  ngtmnft  10755  qsqueeze  10787  qextlt  10789  qextle  10790  icoshft  11019  injresinj  11200  rexuzre  12156  rexico  12157  summo  12511  rpnnen2  12825  divalglem5  12917  ndvdssub  12927  pc2dvds  13252  infpn2  13281  vdwnnlem3  13365  mreiincl  13821  joinlem  14447  meetlem  14454  ablfac1eulem  15630  lbsextlem3  16232  xrsdsreclb  16745  znleval  16835  elcls3  17147  isclo2  17152  tgcn  17316  cnprest  17353  ordthaus  17448  hauscmplem  17469  kgencn2  17589  prdstopn  17660  xkohaus  17685  qtoptop2  17731  filufint  17952  fclsbas  18053  alexsubALTlem3  18080  alexsubALTlem4  18081  ptcmplem2  18084  cldsubg  18140  isucn2  18309  metequiv2  18540  bcthlem5  19281  vieta1  20229  aannenlem2  20246  ulmbdd  20314  angpined  20671  rlimcnp2  20805  amgm  20829  ftalem3  20857  bposlem6  21073  cusgrares  21481  rngosn3  22014  lnon0  22299  ocnel  22800  h1dn0  23054  cnlnssadj  23583  cvnbtwn2  23790  cvnbtwn3  23791  cvnbtwn4  23792  dmdbr2  23806  dmdbr3  23808  dmdbr4  23809  superpos  23857  atcvati  23889  mdsymlem4  23909  sumdmdii  23918  cdj3lem1  23937  elicoelioo  24141  erdszelem9  24885  untangtr  25163  3orel2  25165  dfon2lem6  25415  dfon2lem7  25416  nofv  25612  sltres  25619  nodenselem4  25639  nodenselem7  25642  outsideofrflx  26061  mblfinlem2  26244  trer  26319  elicc3  26320  nn0prpw  26326  comppfsc  26387  sdclem1  26447  fdc  26449  incsequz  26452  0rngo  26637  dmncan1  26686  bicomdd  26689  prtlem90  26706  prtlem15  26724  rngunsnply  27355  psgnunilem4  27397  stoweidlem62  27787  atbiffatnnb  27857  2reu3  27942  frgraun  28386  usgreg2spot  28456  ssralv2  28615  truniALT  28626  onfrALTlem3  28630  onfrALTlem2  28632  onfrALTlem1  28634  a9e2ndeq  28646  bnj1280  29389  ax12olem6NEW7  29459  ax15NEW7  29536  ax7w15lemxAUX7  29666  cbvexdOLD7  29735  lsatcvat  29848  lfl1  29868  hlrelat2  30200  cvrat  30219  linepsubN  30549  2llnma3r  30585  dihjatcclem4  32219  dochexmidlem1  32258
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator