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  3079  oteqex  4259  epelg  4306  ordsucuniel  4615  ordsucun  4616  relbrcnvg  5052  brtpos2  6240  eceqoveq  6763  elpmg  6786  elfi2  7168  brwdom  7281  brwdomn0  7283  rankr1c  7493  r1pwcl  7519  ttukeylem1  8136  fpwwe2lem9  8260  eltskm  8465  recmulnq  8588  clim  11968  rlim  11969  lo1o1  12006  o1lo1  12011  o1lo12  12012  rlimresb  12039  lo1eq  12042  rlimeq  12043  isercolllem2  12139  caucvgb  12152  saddisj  12656  sadadd  12658  sadass  12662  bitsshft  12666  smupvallem  12674  smumul  12684  catpropd  13612  isssc  13697  issubc  13712  funcres2b  13771  funcres2c  13775  mndpropd  14398  issubg3  14637  resghm2b  14701  elsymgbas  14774  resscntz  14807  odmulg  14869  dmdprd  15236  dprdw  15245  subgdmdprd  15269  lmodprop2d  15687  lssacs  15724  assapropd  16067  psrbaglefi  16118  prmirred  16448  cnrest2  17014  cnprest  17017  cnprest2  17018  lmss  17026  isfildlem  17552  isfcls  17704  dscopn  18096  iscau2  18703  causs  18724  ismbf  18985  ismbfcn  18986  iblcnlem  19143  limcdif  19226  limcres  19236  limcun  19245  dvres  19261  q1peqb  19540  ulmval  19759  ulmres  19767  chpchtsum  20458  dchrisum0lem1  20665  ismndo2  21012  isrngo  21045  cvmlift3lem4  23853  iseupa  23881  axcontlem5  24596  brcolinear2  24681  topfneec  26291  cnpwstotbnd  26521  ismtyima  26527  elrfi  26769  lindfmm  27297  lsslindf  27300  islinds3  27304  lshpkr  29307
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