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  900  rmob  3416  oteqex  4730  epelg  4782  eqbrrdva  5162  relbrcnvg  5365  ordsucuniel  6644  ordsucun  6645  brtpos2  6963  eceqoveq  7418  elpmg  7436  elfi2  7876  brwdom  7996  brwdomn0  7998  rankr1c  8242  r1pwcl  8268  ttukeylem1  8892  fpwwe2lem9  9019  eltskm  9224  recmulnq  9345  clim  13299  rlim  13300  lo1o1  13337  o1lo1  13342  o1lo12  13343  rlimresb  13370  lo1eq  13373  rlimeq  13374  isercolllem2  13470  caucvgb  13484  saddisj  14097  sadadd  14099  sadass  14103  bitsshft  14107  smupvallem  14115  smumul  14125  catpropd  15086  isssc  15171  issubc  15186  funcres2b  15245  funcres2c  15249  mndpropd  15925  issubg3  16198  resghm2b  16264  resscntz  16348  elsymgbas  16386  odmulg  16557  dmdprd  17008  dprdw  17022  dprdwOLD  17029  subgdmdprd  17060  lmodprop2d  17551  lssacs  17592  assapropd  17955  psrbaglefi  18002  psrbaglefiOLD  18003  prmirred  18503  prmirredOLD  18506  lindfmm  18840  lsslindf  18843  islinds3  18847  cnrest2  19765  cnprest  19768  cnprest2  19769  lmss  19777  isfildlem  20336  isfcls  20488  elutop  20714  metustelOLD  21032  metustel  21033  blval2  21056  dscopn  21072  iscau2  21694  causs  21715  ismbf  22015  ismbfcn  22016  iblcnlem  22173  limcdif  22258  limcres  22268  limcun  22277  dvres  22293  q1peqb  22533  ulmval  22753  ulmres  22761  chpchtsum  23472  dchrisum0lem1  23679  axcontlem5  24249  iseupa  24943  ismndo2  25325  isrngo  25358  issiga  28089  ismeas  28148  cvmlift3lem4  28745  msrrcl  28881  brcolinear2  29684  topfneec  30149  cnpwstotbnd  30269  ismtyima  30275  elrfi  30602  climf  31582  lshpkr  34717