Theorem pm5.21ndd 356

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 139	. . 3 |- ( ph -> ( -. ps -> -. ch ) )
4		pm5.21ndd.2	. . . 4 |- ( ph -> ( th -> ps ) )
5	4	con3d 139	. . 3 |- ( ph -> ( -. ps -> -. th ) )
6		pm5.21im 351	. . 3 |- ( -. ch -> ( -. th -> ( ch <-> th ) ) )
7	3, 5, 6	syl6c 66	. 2 |- ( ph -> ( -. ps -> ( ch <-> th ) ) )
8	1, 7	pm2.61d 162	1 |- ( ph -> ( ch <-> th ) )

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

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 189

This theorem is referenced by:  pm5.21nd  910  rmob  3358  oteqex  4693  epelg  4745  eqbrrdva  5003  relbrcnvg  5207  ordsucuniel  6648  ordsucun  6649  brtpos2  6976  eceqoveq  7465  elpmg  7484  elfi2  7925  brwdom  8079  brwdomn0  8081  rankr1c  8289  r1pwcl  8315  ttukeylem1  8936  fpwwe2lem9  9060  eltskm  9265  recmulnq  9386  clim  13551  rlim  13552  lo1o1  13589  o1lo1  13594  o1lo12  13595  rlimresb  13622  lo1eq  13625  rlimeq  13626  isercolllem2  13722  caucvgb  13739  saddisj  14432  sadadd  14434  sadass  14438  bitsshft  14442  smupvallem  14450  smumul  14460  catpropd  15607  isssc  15718  issubc  15733  funcres2b  15795  funcres2c  15799  mndpropd  16555  issubg3  16828  resghm2b  16894  resscntz  16978  elsymgbas  17016  odmulg  17200  dmdprd  17623  dprdw  17635  subgdmdprd  17660  lmodprop2d  18143  lssacs  18183  assapropd  18544  psrbaglefi  18589  prmirred  19059  lindfmm  19378  lsslindf  19381  islinds3  19385  cnrest2  20295  cnprest  20298  cnprest2  20299  lmss  20307  isfildlem  20865  isfcls  21017  elutop  21241  metustel  21558  blval2  21570  dscopn  21581  iscau2  22240  causs  22261  ismbf  22579  ismbfcn  22580  iblcnlem  22739  limcdif  22824  limcres  22834  limcun  22843  dvres  22859  q1peqb  23098  ulmval  23328  ulmres  23336  chpchtsum  24140  dchrisum0lem1  24347  axcontlem5  24991  iseupa  25686  ismndo2  26066  isrngo  26099  issiga  28926  ismeas  29014  elcarsg  29130  cvmlift3lem4  30038  msrrcl  30174  brcolinear2  30818  topfneec  31004  cnpwstotbnd  32122  ismtyima  32128  lshpkr  32677  elrfi  35530  climf  37696  is1wlkg  39614