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  2999  abvor0  3472  ralidm  3557  disjprg  4019  euotd  4267  posn  4758  frsn  4760  cnvpo  5213  elabrex  5765  riota5f  6329  smoord  6382  brwdom2  7287  finacn  7677  acacni  7766  dfac13  7768  fin1a2lem10  8035  gchac  8295  gch2  8301  recmulnq  8588  nn1m1nn  9766  nn0sub  10014  qextltlem  10529  xsubge0  10581  xlesubadd  10583  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  sqlecan  11209  nnesq  11225  hashdom  11361  znnenlem  12490  bitsmod  12627  dvdssq  12739  pcdvdsb  12921  vdwmc2  13026  acsfn  13561  subsubc  13727  funcres2b  13771  isipodrs  14264  issubg3  14637  opnnei  16857  lmss  17026  lmres  17028  cmpfi  17135  xkopt  17349  acufl  17612  lmhmclm  18584  equivcmet  18741  degltlem1  19458  mdegle0  19463  cxple2  20044  rlimcnp3  20262  dchrelbas3  20477  isoun  23242  eupath2lem3  23903  fz0n  24097  onint1  24888  wl-pm5.74  24918  gicabl  27263  dfacbasgrp  27273  sdrgacs  27509  lcvexchlem1  29224  ltrnatb  30326  cdlemg27b  30885
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