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  888  rmob  3283  oteqex  4581  epelg  4629  eqbrrdva  5005  relbrcnvg  5204  ordsucuniel  6434  ordsucun  6435  brtpos2  6750  eceqoveq  7201  elpmg  7224  elfi2  7660  brwdom  7778  brwdomn0  7780  rankr1c  8024  r1pwcl  8050  ttukeylem1  8674  fpwwe2lem9  8801  eltskm  9006  recmulnq  9129  clim  12968  rlim  12969  lo1o1  13006  o1lo1  13011  o1lo12  13012  rlimresb  13039  lo1eq  13042  rlimeq  13043  isercolllem2  13139  caucvgb  13153  saddisj  13657  sadadd  13659  sadass  13663  bitsshft  13667  smupvallem  13675  smumul  13685  catpropd  14644  isssc  14729  issubc  14744  funcres2b  14803  funcres2c  14807  mndpropd  15442  issubg3  15692  resghm2b  15758  resscntz  15842  elsymgbas  15880  odmulg  16050  dmdprd  16470  dprdw  16484  dprdwOLD  16490  subgdmdprd  16521  lmodprop2d  16987  lssacs  17026  assapropd  17376  psrbaglefi  17419  psrbaglefiOLD  17420  prmirred  17878  prmirredOLD  17881  lindfmm  18215  lsslindf  18218  islinds3  18222  cnrest2  18849  cnprest  18852  cnprest2  18853  lmss  18861  isfildlem  19389  isfcls  19541  elutop  19767  metustelOLD  20085  metustel  20086  blval2  20109  dscopn  20125  iscau2  20747  causs  20768  ismbf  21067  ismbfcn  21068  iblcnlem  21225  limcdif  21310  limcres  21320  limcun  21329  dvres  21345  q1peqb  21585  ulmval  21804  ulmres  21812  chpchtsum  22517  dchrisum0lem1  22724  axcontlem5  23149  iseupa  23521  ismndo2  23767  isrngo  23800  issiga  26490  ismeas  26549  cvmlift3lem4  27141  brcolinear2  28018  topfneec  28488  cnpwstotbnd  28621  ismtyima  28627  elrfi  28955  lshpkr  32484