Theorem pm5.21ndd 354

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 349	. . 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  893  rmob  3301  oteqex  4599  epelg  4648  eqbrrdva  5024  relbrcnvg  5222  ordsucuniel  6450  ordsucun  6451  brtpos2  6766  eceqoveq  7220  elpmg  7243  elfi2  7679  brwdom  7797  brwdomn0  7799  rankr1c  8043  r1pwcl  8069  ttukeylem1  8693  fpwwe2lem9  8820  eltskm  9025  recmulnq  9148  clim  12987  rlim  12988  lo1o1  13025  o1lo1  13030  o1lo12  13031  rlimresb  13058  lo1eq  13061  rlimeq  13062  isercolllem2  13158  caucvgb  13172  saddisj  13676  sadadd  13678  sadass  13682  bitsshft  13686  smupvallem  13694  smumul  13704  catpropd  14663  isssc  14748  issubc  14763  funcres2b  14822  funcres2c  14826  mndpropd  15461  issubg3  15714  resghm2b  15780  resscntz  15864  elsymgbas  15902  odmulg  16072  dmdprd  16495  dprdw  16509  dprdwOLD  16515  subgdmdprd  16546  lmodprop2d  17022  lssacs  17063  assapropd  17413  psrbaglefi  17456  psrbaglefiOLD  17457  prmirred  17934  prmirredOLD  17937  lindfmm  18271  lsslindf  18274  islinds3  18278  cnrest2  18905  cnprest  18908  cnprest2  18909  lmss  18917  isfildlem  19445  isfcls  19597  elutop  19823  metustelOLD  20141  metustel  20142  blval2  20165  dscopn  20181  iscau2  20803  causs  20824  ismbf  21123  ismbfcn  21124  iblcnlem  21281  limcdif  21366  limcres  21376  limcun  21385  dvres  21401  q1peqb  21641  ulmval  21860  ulmres  21868  chpchtsum  22573  dchrisum0lem1  22780  axcontlem5  23229  iseupa  23601  ismndo2  23847  isrngo  23880  issiga  26569  ismeas  26628  cvmlift3lem4  27226  brcolinear2  28104  topfneec  28582  cnpwstotbnd  28715  ismtyima  28721  elrfi  29049  lshpkr  32781