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  898  rmob  3431  oteqex  4740  epelg  4792  eqbrrdva  5170  relbrcnvg  5373  ordsucuniel  6637  ordsucun  6638  brtpos2  6958  eceqoveq  7413  elpmg  7431  elfi2  7870  brwdom  7989  brwdomn0  7991  rankr1c  8235  r1pwcl  8261  ttukeylem1  8885  fpwwe2lem9  9012  eltskm  9217  recmulnq  9338  clim  13276  rlim  13277  lo1o1  13314  o1lo1  13319  o1lo12  13320  rlimresb  13347  lo1eq  13350  rlimeq  13351  isercolllem2  13447  caucvgb  13461  saddisj  13970  sadadd  13972  sadass  13976  bitsshft  13980  smupvallem  13988  smumul  13998  catpropd  14961  isssc  15046  issubc  15061  funcres2b  15120  funcres2c  15124  mndpropd  15759  issubg3  16014  resghm2b  16080  resscntz  16164  elsymgbas  16202  odmulg  16374  dmdprd  16820  dprdw  16834  dprdwOLD  16840  subgdmdprd  16871  lmodprop2d  17355  lssacs  17396  assapropd  17747  psrbaglefi  17794  psrbaglefiOLD  17795  prmirred  18292  prmirredOLD  18295  lindfmm  18629  lsslindf  18632  islinds3  18636  cnrest2  19553  cnprest  19556  cnprest2  19557  lmss  19565  isfildlem  20093  isfcls  20245  elutop  20471  metustelOLD  20789  metustel  20790  blval2  20813  dscopn  20829  iscau2  21451  causs  21472  ismbf  21772  ismbfcn  21773  iblcnlem  21930  limcdif  22015  limcres  22025  limcun  22034  dvres  22050  q1peqb  22290  ulmval  22509  ulmres  22517  chpchtsum  23222  dchrisum0lem1  23429  axcontlem5  23947  iseupa  24641  ismndo2  25023  isrngo  25056  opeldifid  27129  issiga  27751  ismeas  27810  cvmlift3lem4  28407  brcolinear2  29285  topfneec  29763  cnpwstotbnd  29896  ismtyima  29902  elrfi  30230  climf  31164  lshpkr  33914