MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ib 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  1814  19.23hOLD  1829  ax12olem6OLD  1962  cbvexd  2035  ax15  2047  2eu3  2313  exists2  2321  necon2bd  2592  necon2d  2593  necon4ad  2604  necon4d  2606  necon1bd  2611  spcimgft  2963  eqsbc3r  3154  reupick  3561  prneimg  3913  invdisj  4135  trin  4246  pwssun  4423  wefrc  4510  ordtri3  4551  suc11  4618  onmindif2  4725  eqbrrdva  4975  elreldm  5027  elres  5114  xp11  5237  ssrnres  5242  opelf  5539  dffo4  5817  dftpos3  6426  swoer  6862  mapsn  6984  domtriord  7182  nneneq  7219  unblem1  7288  supnub  7393  suc11reg  7500  inf3lem2  7510  trcl  7590  en3lplem2  7597  tz9.13  7643  acndom  7858  carduniima  7903  cardinfima  7904  dfac5lem5  7934  fin23lem26  8131  hsmexlem2  8233  axcc4  8245  axdc3lem2  8257  axdclem2  8326  entric  8358  alephval2  8373  cfpwsdom  8385  fpwwe2lem9  8439  ltapr  8848  supsrlem  8912  sup2  9889  nnunb  10142  nneo  10278  indstr  10470  ngtmnft  10680  qsqueeze  10712  qextlt  10714  qextle  10715  icoshft  10944  injresinj  11120  rexuzre  12076  rexico  12077  summo  12431  rpnnen2  12745  divalglem5  12837  ndvdssub  12847  pc2dvds  13172  infpn2  13201  vdwnnlem3  13285  mreiincl  13741  joinlem  14367  meetlem  14374  ablfac1eulem  15550  lbsextlem3  16152  xrsdsreclb  16661  znleval  16751  elcls3  17063  isclo2  17068  tgcn  17231  cnprest  17268  ordthaus  17363  hauscmplem  17384  kgencn2  17503  prdstopn  17574  xkohaus  17599  qtoptop2  17645  filufint  17866  fclsbas  17967  alexsubALTlem3  17994  alexsubALTlem4  17995  ptcmplem2  17998  cldsubg  18054  isucn2  18223  metequiv2  18423  bcthlem5  19143  vieta1  20089  aannenlem2  20106  ulmbdd  20174  angpined  20531  rlimcnp2  20665  amgm  20689  ftalem3  20717  bposlem6  20933  cusgrares  21340  rngosn3  21855  lnon0  22140  ocnel  22641  h1dn0  22895  cnlnssadj  23424  cvnbtwn2  23631  cvnbtwn3  23632  cvnbtwn4  23633  dmdbr2  23647  dmdbr3  23649  dmdbr4  23650  superpos  23698  atcvati  23730  mdsymlem4  23750  sumdmdii  23759  cdj3lem1  23778  elicoelioo  23970  erdszelem9  24657  untangtr  24935  3orel2  24937  dfon2lem6  25161  dfon2lem7  25162  nofv  25328  sltres  25335  nodenselem4  25355  nodenselem7  25358  outsideofrflx  25768  trer  26003  elicc3  26004  nn0prpw  26010  comppfsc  26071  sdclem1  26131  fdc  26133  incsequz  26136  0rngo  26321  dmncan1  26370  bicomdd  26373  prtlem90  26390  prtlem15  26408  rngunsnply  27040  psgnunilem4  27082  stoweidlem62  27472  atbiffatnnb  27542  2reu3  27627  frgraun  27742  ssralv2  27951  truniALT  27962  onfrALTlem3  27966  onfrALTlem2  27968  onfrALTlem1  27970  a9e2ndeq  27982  bnj1280  28720  ax12olem6NEW7  28790  ax15NEW7  28865  cbvexdOLD7  29044  a12study2  29110  a12study10  29112  a12study10n  29113  lsatcvat  29216  lfl1  29236  hlrelat2  29568  cvrat  29587  linepsubN  29917  2llnma3r  29953  dihjatcclem4  31587  dochexmidlem1  31626
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