Theorem pm5.21ndd 378

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 373	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 179	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

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

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 206

This theorem is referenced by:  pm5.21nd  798  sbcrext  3866  rmob  3883  elpr2g  4651  oteqex  5499  epelg  5580  eqbrrdva  5868  relbrcnvg  6103  ordsucuniel  7814  ordsucun  7815  xpord2pred  8133  brtpos2  8219  eceqoveq  8818  elpmg  8839  elfi2  9411  brwdom  9564  brwdomn0  9566  rankr1c  9818  r1pwcl  9844  ttukeylem1  10506  fpwwe2lem8  10635  eltskm  10840  recmulnq  10961  clim  15442  rlim  15443  lo1o1  15480  o1lo1  15485  o1lo12  15486  rlimresb  15513  lo1eq  15516  rlimeq  15517  isercolllem2  15616  caucvgb  15630  saddisj  16410  sadadd  16412  sadass  16416  bitsshft  16420  smupvallem  16428  smumul  16438  catpropd  17657  isssc  17771  issubc  17789  funcres2b  17851  funcres2c  17856  sgrppropd  18656  mndpropd  18684  issubg3  19060  resghm2b  19148  resscntz  19238  elsymgbas  19282  odmulg  19465  dmdprd  19909  dprdw  19921  subgdmdprd  19945  lmodprop2d  20678  lssacs  20722  prmirred  21245  lindfmm  21601  lsslindf  21604  islinds3  21608  assapropd  21645  psrbaglefi  21704  psrbaglefiOLD  21705  cnrest2  23010  cnprest  23013  cnprest2  23014  lmss  23022  isfildlem  23581  isfcls  23733  elutop  23958  metustel  24279  blval2  24291  dscopn  24302  iscau2  25025  causs  25046  ismbf  25377  ismbfcn  25378  iblcnlem  25538  limcdif  25625  limcres  25635  limcun  25644  dvres  25660  q1peqb  25907  ulmval  26128  ulmres  26136  chpchtsum  26958  dchrisum0lem1  27255  elmade  27599  axcontlem5  28493  iswlkg  29137  issiga  33408  ismeas  33495  elcarsg  33602  cvmlift3lem4  34611  msrrcl  34832  brcolinear2  35334  topfneec  35543  bj-epelg  36252  cnpwstotbnd  36968  ismtyima  36974  ismndo2  37045  isrngo  37068  lshpkr  38290  elrfi  41734  climf  44636  climf2  44680  isupwlkg  46813