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

Theorem 2thd 232
Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)
Hypotheses
Ref Expression
2thd.1  |-  ( ph  ->  ps )
2thd.2  |-  ( ph  ->  ch )
Assertion
Ref Expression
2thd  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem 2thd
StepHypRef Expression
1 2thd.1 . 2  |-  ( ph  ->  ps )
2 2thd.2 . 2  |-  ( ph  ->  ch )
3 pm5.1im 230 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 58 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  had1  1411  sbc2or  3169  abvor0  3645  ralidm  3731  disjprg  4208  euotd  4457  posn  4946  frsn  4948  cnvpo  5410  elabrex  5985  riota5f  6574  smoord  6627  brwdom2  7541  finacn  7931  acacni  8020  dfac13  8022  fin1a2lem10  8289  gchac  8548  gch2  8554  recmulnq  8841  nn1m1nn  10020  nn0sub  10270  qextltlem  10788  xsubge0  10840  xlesubadd  10842  iccshftr  11030  iccshftl  11032  iccdil  11034  icccntr  11036  fzaddel  11087  sqlecan  11487  nnesq  11503  hashdom  11653  znnenlem  12811  bitsmod  12948  dvdssq  13060  pcdvdsb  13242  vdwmc2  13347  acsfn  13884  subsubc  14050  funcres2b  14094  isipodrs  14587  issubg3  14960  opnnei  17184  lmss  17362  lmres  17364  cmpfi  17471  xkopt  17687  acufl  17949  lmhmclm  19111  equivcmet  19268  degltlem1  19995  mdegle0  20000  cxple2  20588  rlimcnp3  20806  dchrelbas3  21022  eupath2lem3  21701  isoun  24089  fz0n  25202  onint1  26199  wl-pm5.74  26228  ftc1anclem6  26285  gicabl  27240  dfacbasgrp  27250  sdrgacs  27486  elfzomelpfzo  28129  lcvexchlem1  29832  ltrnatb  30934  cdlemg27b  31493
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