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 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

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

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 210

This theorem is referenced by:  pm5.21nd  813  sbcrext  3829  rmob  3846  elpr2g  4611  oteqex  5474  epelg  5553  eqbrrdva  5846  relbrcnvg  6098  ordsucuniel  7808  ordsucun  7809  xpord2pred  8129  brtpos2  8216  eceqoveq  8808  elpmg  8828  elfi2  9362  brwdom  9517  brwdomn0  9519  rankr1c  9781  r1pwcl  9807  ttukeylem1  10481  fpwwe2lem8  10611  eltskm  10816  recmulnq  10937  clim  15535  rlim  15536  lo1o1  15573  o1lo1  15578  o1lo12  15579  rlimresb  15606  lo1eq  15609  rlimeq  15610  isercolllem2  15707  caucvgb  15721  saddisj  16513  sadadd  16515  sadass  16519  bitsshft  16523  smupvallem  16531  smumul  16541  catpropd  17755  isssc  17867  issubc  17882  funcres2b  17944  funcres2c  17950  sgrppropd  18779  mndpropd  18807  issubg3  19202  resghm2b  19295  resscntz  19394  elsymgbas  19435  odmulg  19617  dmdprd  20061  dprdw  20073  subgdmdprd  20097  lmodprop2d  21014  lssacs  21057  prmirred  21584  lindfmm  21937  lsslindf  21940  islinds3  21944  assapropd  21981  psrbaglefi  22036  cnrest2  23404  cnprest  23407  cnprest2  23408  lmss  23416  isfildlem  23975  isfcls  24127  elutop  24351  metustel  24668  blval2  24680  dscopn  24691  iscau2  25397  causs  25418  ismbf  25748  ismbfcn  25749  iblcnlem  25909  limcdif  25996  limcres  26006  limcun  26015  dvres  26031  q1peqb  26274  ulmval  26501  ulmres  26509  chpchtsum  27341  dchrisum0lem1  27638  elmade  28008  axcontlem5  29227  iswlkg  29872  issiga  34419  ismeas  34506  elcarsg  34612  cvmlift3lem4  35685  msrrcl  35906  brcolinear2  36421  topfneec  36728  bj-epelg  37565  cnpwstotbnd  38308  ismtyima  38314  ismndo2  38385  isrngo  38408  lshpkr  39753  fimgmcyc  43164  elrfi  43287  traxext  45551  climf  46196  climf2  46238  isupwlkg  48757