Theorem pm5.21ndd 368

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

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

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 197

This theorem is referenced by:  pm5.21nd  961  sbcrext  3544  rmob  3562  oteqex  4993  epelg  5059  eqbrrdva  5324  relbrcnvg  5539  ordsucuniel  7066  ordsucun  7067  brtpos2  7403  eceqoveq  7895  elpmg  7915  elfi2  8361  brwdom  8513  brwdomn0  8515  rankr1c  8722  r1pwcl  8748  ttukeylem1  9369  fpwwe2lem9  9498  eltskm  9703  recmulnq  9824  clim  14269  rlim  14270  lo1o1  14307  o1lo1  14312  o1lo12  14313  rlimresb  14340  lo1eq  14343  rlimeq  14344  isercolllem2  14440  caucvgb  14454  saddisj  15234  sadadd  15236  sadass  15240  bitsshft  15244  smupvallem  15252  smumul  15262  catpropd  16416  isssc  16527  issubc  16542  funcres2b  16604  funcres2c  16608  mndpropd  17363  issubg3  17659  resghm2b  17725  resscntz  17810  elsymgbas  17848  odmulg  18019  dmdprd  18443  dprdw  18455  subgdmdprd  18479  lmodprop2d  18973  lssacs  19015  assapropd  19375  psrbaglefi  19420  prmirred  19891  lindfmm  20214  lsslindf  20217  islinds3  20221  cnrest2  21138  cnprest  21141  cnprest2  21142  lmss  21150  isfildlem  21708  isfcls  21860  elutop  22084  metustel  22402  blval2  22414  dscopn  22425  iscau2  23121  causs  23142  ismbf  23442  ismbfcn  23443  iblcnlem  23600  limcdif  23685  limcres  23695  limcun  23704  dvres  23720  q1peqb  23959  ulmval  24179  ulmres  24187  chpchtsum  24989  dchrisum0lem1  25250  axcontlem5  25893  iswlkg  26565  issiga  30302  ismeas  30390  elcarsg  30495  cvmlift3lem4  31430  msrrcl  31566  brcolinear2  32290  topfneec  32475  cnpwstotbnd  33726  ismtyima  33732  ismndo2  33803  isrngo  33826  lshpkr  34722  elrfi  37574  climf  40172  climf2  40216  isupwlkg  42043