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

Theorem pm5.21ndd 343
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.)
Hypotheses
Ref Expression
pm5.21ndd.1  |-  ( ph  ->  ( ch  ->  ps ) )
pm5.21ndd.2  |-  ( ph  ->  ( th  ->  ps ) )
pm5.21ndd.3  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.21ndd  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem pm5.21ndd
StepHypRef Expression
1 pm5.21ndd.3 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
2 pm5.21ndd.1 . . . 4  |-  ( ph  ->  ( ch  ->  ps ) )
32con3d 125 . . 3  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
4 pm5.21ndd.2 . . . 4  |-  ( ph  ->  ( th  ->  ps ) )
54con3d 125 . . 3  |-  ( ph  ->  ( -.  ps  ->  -. 
th ) )
6 pm5.21im 338 . . 3  |-  ( -. 
ch  ->  ( -.  th  ->  ( ch  <->  th )
) )
73, 5, 6syl6c 60 . 2  |-  ( ph  ->  ( -.  ps  ->  ( ch  <->  th ) ) )
81, 7pm2.61d 150 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  pm5.21nd  868  rmob  3092  oteqex  4275  epelg  4322  ordsucuniel  4631  ordsucun  4632  relbrcnvg  5068  brtpos2  6256  eceqoveq  6779  elpmg  6802  elfi2  7184  brwdom  7297  brwdomn0  7299  rankr1c  7509  r1pwcl  7535  ttukeylem1  8152  fpwwe2lem9  8276  eltskm  8481  recmulnq  8604  clim  11984  rlim  11985  lo1o1  12022  o1lo1  12027  o1lo12  12028  rlimresb  12055  lo1eq  12058  rlimeq  12059  isercolllem2  12155  caucvgb  12168  saddisj  12672  sadadd  12674  sadass  12678  bitsshft  12682  smupvallem  12690  smumul  12700  catpropd  13628  isssc  13713  issubc  13728  funcres2b  13787  funcres2c  13791  mndpropd  14414  issubg3  14653  resghm2b  14717  elsymgbas  14790  resscntz  14823  odmulg  14885  dmdprd  15252  dprdw  15261  subgdmdprd  15285  lmodprop2d  15703  lssacs  15740  assapropd  16083  psrbaglefi  16134  prmirred  16464  cnrest2  17030  cnprest  17033  cnprest2  17034  lmss  17042  isfildlem  17568  isfcls  17720  dscopn  18112  iscau2  18719  causs  18740  ismbf  19001  ismbfcn  19002  iblcnlem  19159  limcdif  19242  limcres  19252  limcun  19261  dvres  19277  q1peqb  19556  ulmval  19775  ulmres  19783  chpchtsum  20474  dchrisum0lem1  20681  ismndo2  21028  isrngo  21061  cvmlift3lem4  23868  iseupa  23896  axcontlem5  24668  brcolinear2  24753  topfneec  26394  cnpwstotbnd  26624  ismtyima  26630  elrfi  26872  lindfmm  27400  lsslindf  27403  islinds3  27407  lshpkr  29929
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