Theorem pm5.21ndd 344

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

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

This theorem is referenced by:  pm5.21nd  869  rmob  3209  oteqex  4409  epelg  4455  ordsucuniel  4763  ordsucun  4764  eqbrrdva  5001  relbrcnvg  5202  brtpos2  6444  eceqoveq  6968  elpmg  6991  elfi2  7377  brwdom  7491  brwdomn0  7493  rankr1c  7703  r1pwcl  7729  ttukeylem1  8345  fpwwe2lem9  8469  eltskm  8674  recmulnq  8797  clim  12243  rlim  12244  lo1o1  12281  o1lo1  12286  o1lo12  12287  rlimresb  12314  lo1eq  12317  rlimeq  12318  isercolllem2  12414  caucvgb  12428  saddisj  12932  sadadd  12934  sadass  12938  bitsshft  12942  smupvallem  12950  smumul  12960  catpropd  13890  isssc  13975  issubc  13990  funcres2b  14049  funcres2c  14053  mndpropd  14676  issubg3  14915  resghm2b  14979  elsymgbas  15052  resscntz  15085  odmulg  15147  dmdprd  15514  dprdw  15523  subgdmdprd  15547  lmodprop2d  15961  lssacs  15998  assapropd  16341  psrbaglefi  16392  prmirred  16730  cnrest2  17304  cnprest  17307  cnprest2  17308  lmss  17316  isfildlem  17842  isfcls  17994  elutop  18216  metustelOLD  18534  metustel  18535  blval2  18558  dscopn  18574  iscau2  19183  causs  19204  ismbf  19475  ismbfcn  19476  iblcnlem  19633  limcdif  19716  limcres  19726  limcun  19735  dvres  19751  q1peqb  20030  ulmval  20249  ulmres  20257  chpchtsum  20956  dchrisum0lem1  21163  iseupa  21640  ismndo2  21886  isrngo  21919  issiga  24447  ismeas  24506  cvmlift3lem4  24962  axcontlem5  25811  brcolinear2  25896  topfneec  26261  cnpwstotbnd  26396  ismtyima  26402  elrfi  26638  lindfmm  27165  lsslindf  27168  islinds3  27172  lshpkr  29600

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

This theorem depends on definitions:  df-bi 178