Theorem pm5.21ndd 382

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.21nd  814  sbcrext  3819  rmob  3836  elpr2g  4606  oteqex  5471  epelg  5551  eqbrrdva  5846  relbrcnvg  6100  ordsucuniel  7835  ordsucun  7836  xpord2pred  8164  brtpos2  8252  eceqoveq  8846  elpmg  8866  elfi2  9409  brwdom  9564  brwdomn0  9566  rankr1c  9833  r1pwcl  9864  ttukeylem1  10590  fpwwe2lem8  10726  eltskm  10931  recmulnq  11052  clim  15666  rlim  15667  lo1o1  15704  o1lo1  15709  o1lo12  15710  rlimresb  15737  lo1eq  15740  rlimeq  15741  isercolllem2  15838  caucvgb  15852  saddisj  16640  sadadd  16642  sadass  16646  bitsshft  16650  smupvallem  16658  smumul  16668  catpropd  17888  isssc  18000  issubc  18015  funcres2b  18077  funcres2c  18083  sgrppropd  18925  mndpropd  18956  issubg3  19360  resghm2b  19453  resscntz  19552  elsymgbas  19593  odmulg  19775  dmdprd  20219  dprdw  20231  subgdmdprd  20255  lmodprop2d  21204  lssacs  21247  prmirred  21785  lindfmm  22138  lsslindf  22141  islinds3  22145  assapropd  22184  psrbaglefi  22239  cnrest2  23609  cnprest  23612  cnprest2  23613  lmss  23621  isfildlem  24181  isfcls  24333  elutop  24557  metustel  24874  blval2  24886  dscopn  24897  iscau2  25603  causs  25624  ismbf  25954  ismbfcn  25955  iblcnlem  26114  limcdif  26201  limcres  26211  limcun  26220  dvres  26236  q1peqb  26479  ulmval  26712  ulmres  26720  chpchtsum  27551  dchrisum0lem1  27848  elmade  28248  axcontlem5  29551  iswlkg  30199  issiga  34790  ismeas  34878  elcarsg  34983  cvmlift3lem4  36173  msrrcl  36394  brcolinear2  36915  topfneec  37235  bj-epelg  38075  cnpwstotbnd  38824  ismtyima  38830  ismndo2  38901  isrngo  38924  lshpkr  40267  fimgmcyc  43691  elrfi  43798  traxext  46060  climf  46727  climf2  46769  isupwlkg  49328