Theorem pm5.21ndd 380

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

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

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 208

This theorem is referenced by:  pm5.21nd  807  sbcrext  3812  rmob  3829  elpr2g  4588  oteqex  5448  epelg  5526  eqbrrdva  5818  relbrcnvg  6064  ordsucuniel  7771  ordsucun  7772  xpord2pred  8092  brtpos2  8179  eceqoveq  8766  elpmg  8787  elfi2  9324  brwdom  9479  brwdomn0  9481  rankr1c  9743  r1pwcl  9769  ttukeylem1  10429  fpwwe2lem8  10559  eltskm  10764  recmulnq  10885  clim  15454  rlim  15455  lo1o1  15492  o1lo1  15497  o1lo12  15498  rlimresb  15525  lo1eq  15528  rlimeq  15529  isercolllem2  15626  caucvgb  15640  saddisj  16432  sadadd  16434  sadass  16438  bitsshft  16442  smupvallem  16450  smumul  16460  catpropd  17673  isssc  17785  issubc  17800  funcres2b  17862  funcres2c  17868  sgrppropd  18697  mndpropd  18725  issubg3  19118  resghm2b  19207  resscntz  19306  elsymgbas  19347  odmulg  19529  dmdprd  19973  dprdw  19985  subgdmdprd  20009  lmodprop2d  20921  lssacs  20964  prmirred  21456  lindfmm  21809  lsslindf  21812  islinds3  21816  assapropd  21853  psrbaglefi  21908  cnrest2  23276  cnprest  23279  cnprest2  23280  lmss  23288  isfildlem  23847  isfcls  23999  elutop  24223  metustel  24540  blval2  24552  dscopn  24563  iscau2  25269  causs  25290  ismbf  25620  ismbfcn  25621  iblcnlem  25781  limcdif  25868  limcres  25878  limcun  25887  dvres  25903  q1peqb  26146  ulmval  26370  ulmres  26378  chpchtsum  27207  dchrisum0lem1  27504  elmade  27874  axcontlem5  29062  iswlkg  29707  issiga  34303  ismeas  34390  elcarsg  34496  cvmlift3lem4  35557  msrrcl  35778  brcolinear2  36293  topfneec  36590  bj-epelg  37428  cnpwstotbnd  38171  ismtyima  38177  ismndo2  38248  isrngo  38271  lshpkr  39616  fimgmcyc  43027  elrfi  43150  traxext  45428  climf  46074  climf2  46116  isupwlkg  48635