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

Theorem pm5.21ndd 344
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 127 . . 3  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
4 pm5.21ndd.2 . . . 4  |-  ( ph  ->  ( th  ->  ps ) )
54con3d 127 . . 3  |-  ( ph  ->  ( -.  ps  ->  -. 
th ) )
6 pm5.21im 339 . . 3  |-  ( -. 
ch  ->  ( -.  th  ->  ( ch  <->  th )
) )
73, 5, 6syl6c 62 . 2  |-  ( ph  ->  ( -.  ps  ->  ( ch  <->  th ) ) )
81, 7pm2.61d 152 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  pm5.21nd  869  rmob  3241  oteqex  4441  epelg  4487  ordsucuniel  4796  ordsucun  4797  eqbrrdva  5034  relbrcnvg  5235  brtpos2  6477  eceqoveq  7001  elpmg  7024  elfi2  7411  brwdom  7525  brwdomn0  7527  rankr1c  7737  r1pwcl  7763  ttukeylem1  8379  fpwwe2lem9  8503  eltskm  8708  recmulnq  8831  clim  12278  rlim  12279  lo1o1  12316  o1lo1  12321  o1lo12  12322  rlimresb  12349  lo1eq  12352  rlimeq  12353  isercolllem2  12449  caucvgb  12463  saddisj  12967  sadadd  12969  sadass  12973  bitsshft  12977  smupvallem  12985  smumul  12995  catpropd  13925  isssc  14010  issubc  14025  funcres2b  14084  funcres2c  14088  mndpropd  14711  issubg3  14950  resghm2b  15014  elsymgbas  15087  resscntz  15120  odmulg  15182  dmdprd  15549  dprdw  15558  subgdmdprd  15582  lmodprop2d  15996  lssacs  16033  assapropd  16376  psrbaglefi  16427  prmirred  16765  cnrest2  17340  cnprest  17343  cnprest2  17344  lmss  17352  isfildlem  17879  isfcls  18031  elutop  18253  metustelOLD  18571  metustel  18572  blval2  18595  dscopn  18611  iscau2  19220  causs  19241  ismbf  19512  ismbfcn  19513  iblcnlem  19670  limcdif  19753  limcres  19763  limcun  19772  dvres  19788  q1peqb  20067  ulmval  20286  ulmres  20294  chpchtsum  20993  dchrisum0lem1  21200  iseupa  21677  ismndo2  21923  isrngo  21956  issiga  24484  ismeas  24543  cvmlift3lem4  24999  axcontlem5  25872  brcolinear2  25957  topfneec  26325  cnpwstotbnd  26460  ismtyima  26466  elrfi  26702  lindfmm  27229  lsslindf  27232  islinds3  27236  lshpkr  29816
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