Theorem pm5.21ndd 352

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

Step	Hyp	Ref	Expression
1		pm5.21ndd.3	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
2		pm5.21ndd.1	. . . 4 |- ( ph -> ( ch -> ps ) )
3	2	con3d 133	. . 3 |- ( ph -> ( -. ps -> -. ch ) )
4		pm5.21ndd.2	. . . 4 |- ( ph -> ( th -> ps ) )
5	4	con3d 133	. . 3 |- ( ph -> ( -. ps -> -. th ) )
6		pm5.21im 347	. . 3 |- ( -. ch -> ( -. th -> ( ch <-> th ) ) )
7	3, 5, 6	syl6c 64	. 2 |- ( ph -> ( -. ps -> ( ch <-> th ) ) )
8	1, 7	pm2.61d 158	1 |- ( ph -> ( ch <-> th ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  pm5.21nd  898  rmob  3344  oteqex  4654  epelg  4706  eqbrrdva  5085  relbrcnvg  5288  ordsucuniel  6558  ordsucun  6559  brtpos2  6879  eceqoveq  7334  elpmg  7353  elfi2  7789  brwdom  7908  brwdomn0  7910  rankr1c  8152  r1pwcl  8178  ttukeylem1  8802  fpwwe2lem9  8927  eltskm  9132  recmulnq  9253  clim  13319  rlim  13320  lo1o1  13357  o1lo1  13362  o1lo12  13363  rlimresb  13390  lo1eq  13393  rlimeq  13394  isercolllem2  13490  caucvgb  13504  saddisj  14117  sadadd  14119  sadass  14123  bitsshft  14127  smupvallem  14135  smumul  14145  catpropd  15115  isssc  15226  issubc  15241  funcres2b  15303  funcres2c  15307  mndpropd  16063  issubg3  16336  resghm2b  16402  resscntz  16486  elsymgbas  16524  odmulg  16695  dmdprd  17142  dprdw  17156  dprdwOLD  17163  subgdmdprd  17194  lmodprop2d  17685  lssacs  17726  assapropd  18089  psrbaglefi  18136  psrbaglefiOLD  18137  prmirred  18625  lindfmm  18947  lsslindf  18950  islinds3  18954  cnrest2  19873  cnprest  19876  cnprest2  19877  lmss  19885  isfildlem  20443  isfcls  20595  elutop  20821  metustelOLD  21139  metustel  21140  blval2  21163  dscopn  21179  iscau2  21801  causs  21822  ismbf  22122  ismbfcn  22123  iblcnlem  22280  limcdif  22365  limcres  22375  limcun  22384  dvres  22400  q1peqb  22640  ulmval  22860  ulmres  22868  chpchtsum  23611  dchrisum0lem1  23818  axcontlem5  24392  iseupa  25086  ismndo2  25464  isrngo  25497  issiga  28260  ismeas  28326  elcarsg  28432  cvmlift3lem4  28956  msrrcl  29092  brcolinear2  29861  topfneec  30339  cnpwstotbnd  30459  ismtyima  30465  elrfi  30792  climf  31794  lshpkr  35255