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  802  sbcrext  3812  rmob  3829  elpr2g  4594  oteqex  5448  epelg  5525  eqbrrdva  5818  relbrcnvg  6064  ordsucuniel  7768  ordsucun  7769  xpord2pred  8088  brtpos2  8175  eceqoveq  8762  elpmg  8783  elfi2  9320  brwdom  9475  brwdomn0  9477  rankr1c  9736  r1pwcl  9762  ttukeylem1  10422  fpwwe2lem8  10552  eltskm  10757  recmulnq  10878  clim  15447  rlim  15448  lo1o1  15485  o1lo1  15490  o1lo12  15491  rlimresb  15518  lo1eq  15521  rlimeq  15522  isercolllem2  15619  caucvgb  15633  saddisj  16425  sadadd  16427  sadass  16431  bitsshft  16435  smupvallem  16443  smumul  16453  catpropd  17666  isssc  17778  issubc  17793  funcres2b  17855  funcres2c  17861  sgrppropd  18690  mndpropd  18718  issubg3  19111  resghm2b  19200  resscntz  19299  elsymgbas  19340  odmulg  19522  dmdprd  19966  dprdw  19978  subgdmdprd  20002  lmodprop2d  20910  lssacs  20953  prmirred  21464  lindfmm  21817  lsslindf  21820  islinds3  21824  assapropd  21861  psrbaglefi  21916  cnrest2  23261  cnprest  23264  cnprest2  23265  lmss  23273  isfildlem  23832  isfcls  23984  elutop  24208  metustel  24525  blval2  24537  dscopn  24548  iscau2  25254  causs  25275  ismbf  25605  ismbfcn  25606  iblcnlem  25766  limcdif  25853  limcres  25863  limcun  25872  dvres  25888  q1peqb  26131  ulmval  26358  ulmres  26366  chpchtsum  27196  dchrisum0lem1  27493  elmade  27863  axcontlem5  29051  iswlkg  29697  issiga  34272  ismeas  34359  elcarsg  34465  cvmlift3lem4  35520  msrrcl  35741  brcolinear2  36256  topfneec  36553  bj-epelg  37391  cnpwstotbnd  38132  ismtyima  38138  ismndo2  38209  isrngo  38232  lshpkr  39577  fimgmcyc  42993  elrfi  43140  traxext  45422  climf  46070  climf2  46112  isupwlkg  48625