Theorem pm5.21ndd 379

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	⊢ (𝜑 → (𝜒 → 𝜓))
pm5.21ndd.2	⊢ (𝜑 → (𝜃 → 𝜓))
pm5.21ndd.3	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.21ndd	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem pm5.21ndd

Step	Hyp	Ref	Expression
1		pm5.21ndd.3	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.21ndd.1	. . . 4 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	con3d 152	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4		pm5.21ndd.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜓))
5	4	con3d 152	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6		pm5.21im 374	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 179	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  pm5.21nd  802  sbcrext  3811  rmob  3828  elpr2g  4593  oteqex  5454  epelg  5532  eqbrrdva  5824  relbrcnvg  6070  ordsucuniel  7775  ordsucun  7776  xpord2pred  8095  brtpos2  8182  eceqoveq  8769  elpmg  8790  elfi2  9327  brwdom  9482  brwdomn0  9484  rankr1c  9745  r1pwcl  9771  ttukeylem1  10431  fpwwe2lem8  10561  eltskm  10766  recmulnq  10887  clim  15456  rlim  15457  lo1o1  15494  o1lo1  15499  o1lo12  15500  rlimresb  15527  lo1eq  15530  rlimeq  15531  isercolllem2  15628  caucvgb  15642  saddisj  16434  sadadd  16436  sadass  16440  bitsshft  16444  smupvallem  16452  smumul  16462  catpropd  17675  isssc  17787  issubc  17802  funcres2b  17864  funcres2c  17870  sgrppropd  18699  mndpropd  18727  issubg3  19120  resghm2b  19209  resscntz  19308  elsymgbas  19349  odmulg  19531  dmdprd  19975  dprdw  19987  subgdmdprd  20011  lmodprop2d  20919  lssacs  20962  prmirred  21454  lindfmm  21807  lsslindf  21810  islinds3  21814  assapropd  21851  psrbaglefi  21906  cnrest2  23251  cnprest  23254  cnprest2  23255  lmss  23263  isfildlem  23822  isfcls  23974  elutop  24198  metustel  24515  blval2  24527  dscopn  24538  iscau2  25244  causs  25265  ismbf  25595  ismbfcn  25596  iblcnlem  25756  limcdif  25843  limcres  25853  limcun  25862  dvres  25878  q1peqb  26121  ulmval  26345  ulmres  26353  chpchtsum  27182  dchrisum0lem1  27479  elmade  27849  axcontlem5  29037  iswlkg  29682  issiga  34256  ismeas  34343  elcarsg  34449  cvmlift3lem4  35504  msrrcl  35725  brcolinear2  36240  topfneec  36537  bj-epelg  37375  cnpwstotbnd  38118  ismtyima  38124  ismndo2  38195  isrngo  38218  lshpkr  39563  fimgmcyc  42979  elrfi  43126  traxext  45404  climf  46052  climf2  46094  isupwlkg  48613