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

Theorem syl6ib 217
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 186 . 2  |-  ( ch 
->  th )
41, 3syl6 29 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3g  260  exp4a  589  mtord  641  19.23h  1740  ax12olem6  1885  cbvexd  1962  ax15  1974  2eu3  2238  exists2  2246  necon2bd  2508  necon2d  2509  necon4ad  2520  necon4d  2522  necon1bd  2527  spcimgft  2872  eqsbc3r  3061  reupick  3465  invdisj  4028  trin  4139  pwssun  4315  wefrc  4403  ordtri3  4444  suc11  4512  onmindif2  4619  elreldm  4919  elres  5006  xp11  5127  ssrnres  5132  opelf  5420  dffo4  5692  dftpos3  6268  swoer  6704  mapsn  6825  domtriord  7023  nneneq  7060  unblem1  7125  supnub  7229  suc11reg  7336  inf3lem2  7346  trcl  7426  en3lplem2  7433  tz9.13  7479  acndom  7694  carduniima  7739  cardinfima  7740  dfac5lem5  7770  fin23lem26  7967  hsmexlem2  8069  axcc4  8081  axdc3lem2  8093  axdclem2  8163  entric  8195  alephval2  8210  cfpwsdom  8222  fpwwe2lem9  8276  ltapr  8685  supsrlem  8749  sup2  9726  nnunb  9977  nneo  10111  indstr  10303  ngtmnft  10512  qsqueeze  10544  qextlt  10546  qextle  10547  icoshft  10774  rexuzre  11852  rexico  11853  summo  12206  rpnnen2  12520  divalglem5  12612  ndvdssub  12622  pc2dvds  12947  infpn2  12976  vdwnnlem3  13060  mreiincl  13514  joinlem  14140  meetlem  14147  ablfac1eulem  15323  lbsextlem3  15929  xrsdsreclb  16434  znleval  16524  elcls3  16836  isclo2  16841  tgcn  16998  cnprest  17033  ordthaus  17128  hauscmplem  17149  kgencn2  17268  prdstopn  17338  xkohaus  17363  qtoptop2  17406  filufint  17631  fclsbas  17732  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem2  17763  cldsubg  17809  metequiv2  18072  bcthlem5  18766  vieta1  19708  aannenlem2  19725  ulmbdd  19791  angpined  20143  rlimcnp2  20277  amgm  20301  ftalem3  20328  bposlem6  20544  rngosn3  21109  lnon0  21392  ocnel  21893  h1dn0  22147  cnlnssadj  22676  cvnbtwn2  22883  cvnbtwn3  22884  cvnbtwn4  22885  dmdbr2  22899  dmdbr3  22901  dmdbr4  22902  superpos  22950  atcvati  22982  mdsymlem4  23002  sumdmdii  23011  cdj3lem1  23030  elicoelioo  23286  erdszelem9  23745  untangtr  24075  3orel2  24077  dfon2lem6  24215  dfon2lem7  24216  nofv  24382  sltres  24389  nodenselem4  24409  nodenselem7  24412  outsideofrflx  24822  oprabex2gpop  25139  islatalg  25286  iintlem1  25713  trer  26330  elicc3  26331  nn0prpw  26342  comppfsc  26410  sdclem1  26556  fdc  26558  incsequz  26561  0rngo  26755  dmncan1  26804  bicomdd  26808  prtlem90  26826  prtlem15  26846  rngunsnply  27481  psgnunilem4  27523  stoweidlem62  27914  2reu3  28069  prneimg  28183  injresinj  28215  ssralv2  28593  truniALT  28604  onfrALTlem3  28608  onfrALTlem2  28610  onfrALTlem1  28612  a9e2ndeq  28624  bnj1280  29366  ax12olem6NEW7  29436  ax15NEW7  29511  cbvexdOLD7  29689  a12study2  29756  a12study10  29758  a12study10n  29759  lsatcvat  29862  lfl1  29882  hlrelat2  30214  cvrat  30233  linepsubN  30563  2llnma3r  30599  dihjatcclem4  32233  dochexmidlem1  32272
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 177
  Copyright terms: Public domain W3C validator