Theorem pm5.21ndd 383

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 155	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4		pm5.21ndd.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜓))
5	4	con3d 155	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6		pm5.21im 377	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 181	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

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

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 209

This theorem is referenced by:  pm5.21nd  800  sbcrext  3856  rmob  3874  oteqex  5390  epelg  5466  epelgOLD  5467  eqbrrdva  5740  relbrcnvg  5968  ordsucuniel  7539  ordsucun  7540  brtpos2  7898  eceqoveq  8402  elpmg  8422  elfi2  8878  brwdom  9031  brwdomn0  9033  rankr1c  9250  r1pwcl  9276  ttukeylem1  9931  fpwwe2lem9  10060  eltskm  10265  recmulnq  10386  clim  14851  rlim  14852  lo1o1  14889  o1lo1  14894  o1lo12  14895  rlimresb  14922  lo1eq  14925  rlimeq  14926  isercolllem2  15022  caucvgb  15036  saddisj  15814  sadadd  15816  sadass  15820  bitsshft  15824  smupvallem  15832  smumul  15842  catpropd  16979  isssc  17090  issubc  17105  funcres2b  17167  funcres2c  17171  mndpropd  17936  issubg3  18297  resghm2b  18376  resscntz  18462  elsymgbas  18502  odmulg  18683  dmdprd  19120  dprdw  19132  subgdmdprd  19156  lmodprop2d  19696  lssacs  19739  assapropd  20101  psrbaglefi  20152  prmirred  20642  lindfmm  20971  lsslindf  20974  islinds3  20978  cnrest2  21894  cnprest  21897  cnprest2  21898  lmss  21906  isfildlem  22465  isfcls  22617  elutop  22842  metustel  23160  blval2  23172  dscopn  23183  iscau2  23880  causs  23901  ismbf  24229  ismbfcn  24230  iblcnlem  24389  limcdif  24474  limcres  24484  limcun  24493  dvres  24509  q1peqb  24748  ulmval  24968  ulmres  24976  chpchtsum  25795  dchrisum0lem1  26092  axcontlem5  26754  iswlkg  27395  issiga  31371  ismeas  31458  elcarsg  31563  cvmlift3lem4  32569  msrrcl  32790  brcolinear2  33519  topfneec  33703  bj-epelg  34363  cnpwstotbnd  35090  ismtyima  35096  ismndo2  35167  isrngo  35190  lshpkr  36268  elrfi  39311  climf  41923  climf2  41967  isupwlkg  44032