Theorem pm5.21ndd 381

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

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

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 206

This theorem is referenced by:  pm5.21nd  801  sbcrext  3868  rmob  3885  elpr2g  4653  oteqex  5501  epelg  5582  eqbrrdva  5870  relbrcnvg  6105  ordsucuniel  7812  ordsucun  7813  xpord2pred  8131  brtpos2  8217  eceqoveq  8816  elpmg  8837  elfi2  9409  brwdom  9562  brwdomn0  9564  rankr1c  9816  r1pwcl  9842  ttukeylem1  10504  fpwwe2lem8  10633  eltskm  10838  recmulnq  10959  clim  15438  rlim  15439  lo1o1  15476  o1lo1  15481  o1lo12  15482  rlimresb  15509  lo1eq  15512  rlimeq  15513  isercolllem2  15612  caucvgb  15626  saddisj  16406  sadadd  16408  sadass  16412  bitsshft  16416  smupvallem  16424  smumul  16434  catpropd  17653  isssc  17767  issubc  17785  funcres2b  17847  funcres2c  17852  sgrppropd  18622  mndpropd  18650  issubg3  19024  resghm2b  19110  resscntz  19197  elsymgbas  19241  odmulg  19424  dmdprd  19868  dprdw  19880  subgdmdprd  19904  lmodprop2d  20534  lssacs  20578  prmirred  21044  lindfmm  21382  lsslindf  21385  islinds3  21389  assapropd  21426  psrbaglefi  21485  psrbaglefiOLD  21486  cnrest2  22790  cnprest  22793  cnprest2  22794  lmss  22802  isfildlem  23361  isfcls  23513  elutop  23738  metustel  24059  blval2  24071  dscopn  24082  iscau2  24794  causs  24815  ismbf  25145  ismbfcn  25146  iblcnlem  25306  limcdif  25393  limcres  25403  limcun  25412  dvres  25428  q1peqb  25672  ulmval  25892  ulmres  25900  chpchtsum  26722  dchrisum0lem1  27019  elmade  27362  axcontlem5  28226  iswlkg  28870  issiga  33110  ismeas  33197  elcarsg  33304  cvmlift3lem4  34313  msrrcl  34534  brcolinear2  35030  topfneec  35240  bj-epelg  35949  cnpwstotbnd  36665  ismtyima  36671  ismndo2  36742  isrngo  36765  lshpkr  37987  elrfi  41432  climf  44338  climf2  44382  isupwlkg  46515