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  801  sbcrext  3836  rmob  3853  elpr2g  4615  oteqex  5460  epelg  5539  eqbrrdva  5833  relbrcnvg  6076  ordsucuniel  7799  ordsucun  7800  xpord2pred  8124  brtpos2  8211  eceqoveq  8795  elpmg  8816  elfi2  9365  brwdom  9520  brwdomn0  9522  rankr1c  9774  r1pwcl  9800  ttukeylem1  10462  fpwwe2lem8  10591  eltskm  10796  recmulnq  10917  clim  15460  rlim  15461  lo1o1  15498  o1lo1  15503  o1lo12  15504  rlimresb  15531  lo1eq  15534  rlimeq  15535  isercolllem2  15632  caucvgb  15646  saddisj  16435  sadadd  16437  sadass  16441  bitsshft  16445  smupvallem  16453  smumul  16463  catpropd  17670  isssc  17782  issubc  17797  funcres2b  17859  funcres2c  17865  sgrppropd  18658  mndpropd  18686  issubg3  19076  resghm2b  19166  resscntz  19265  elsymgbas  19304  odmulg  19486  dmdprd  19930  dprdw  19942  subgdmdprd  19966  lmodprop2d  20830  lssacs  20873  prmirred  21384  lindfmm  21736  lsslindf  21739  islinds3  21743  assapropd  21781  psrbaglefi  21835  cnrest2  23173  cnprest  23176  cnprest2  23177  lmss  23185  isfildlem  23744  isfcls  23896  elutop  24121  metustel  24438  blval2  24450  dscopn  24461  iscau2  25177  causs  25198  ismbf  25529  ismbfcn  25530  iblcnlem  25690  limcdif  25777  limcres  25787  limcun  25796  dvres  25812  q1peqb  26061  ulmval  26289  ulmres  26297  chpchtsum  27130  dchrisum0lem1  27427  elmade  27779  axcontlem5  28895  iswlkg  29541  issiga  34102  ismeas  34189  elcarsg  34296  cvmlift3lem4  35309  msrrcl  35530  brcolinear2  36046  topfneec  36343  bj-epelg  37056  cnpwstotbnd  37791  ismtyima  37797  ismndo2  37868  isrngo  37891  lshpkr  39110  fimgmcyc  42522  elrfi  42682  traxext  44967  climf  45620  climf2  45664  isupwlkg  48125