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

Theorem 2thd 231
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 229 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 56 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  had1  1392  sbc2or  3012  abvor0  3485  ralidm  3570  disjprg  4035  euotd  4283  posn  4774  frsn  4776  cnvpo  5229  elabrex  5781  riota5f  6345  smoord  6398  brwdom2  7303  finacn  7693  acacni  7782  dfac13  7784  fin1a2lem10  8051  gchac  8311  gch2  8317  recmulnq  8604  nn1m1nn  9782  nn0sub  10030  qextltlem  10545  xsubge0  10597  xlesubadd  10599  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  sqlecan  11225  nnesq  11241  hashdom  11377  znnenlem  12506  bitsmod  12643  dvdssq  12755  pcdvdsb  12937  vdwmc2  13042  acsfn  13577  subsubc  13743  funcres2b  13787  isipodrs  14280  issubg3  14653  opnnei  16873  lmss  17042  lmres  17044  cmpfi  17151  xkopt  17365  acufl  17628  lmhmclm  18600  equivcmet  18757  degltlem1  19474  mdegle0  19479  cxple2  20060  rlimcnp3  20278  dchrelbas3  20493  isoun  23257  eupath2lem3  23918  fz0n  24112  onint1  24960  wl-pm5.74  24990  gicabl  27366  dfacbasgrp  27376  sdrgacs  27612  lcvexchlem1  29846  ltrnatb  30948  cdlemg27b  31507
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