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

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

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 209

This theorem is referenced by:  pm5.21nd  811  sbcrext  3826  rmob  3843  elpr2g  4607  oteqex  5468  epelg  5546  eqbrrdva  5839  relbrcnvg  6091  ordsucuniel  7800  ordsucun  7801  xpord2pred  8120  brtpos2  8207  eceqoveq  8799  elpmg  8820  elfi2  9357  brwdom  9512  brwdomn0  9514  rankr1c  9776  r1pwcl  9802  ttukeylem1  10463  fpwwe2lem8  10593  eltskm  10798  recmulnq  10919  clim  15504  rlim  15505  lo1o1  15542  o1lo1  15547  o1lo12  15548  rlimresb  15575  lo1eq  15578  rlimeq  15579  isercolllem2  15676  caucvgb  15690  saddisj  16482  sadadd  16484  sadass  16488  bitsshft  16492  smupvallem  16500  smumul  16510  catpropd  17724  isssc  17836  issubc  17851  funcres2b  17913  funcres2c  17919  sgrppropd  18748  mndpropd  18776  issubg3  19169  resghm2b  19257  resscntz  19356  elsymgbas  19397  odmulg  19579  dmdprd  20023  dprdw  20035  subgdmdprd  20059  lmodprop2d  20971  lssacs  21014  prmirred  21506  lindfmm  21859  lsslindf  21862  islinds3  21866  assapropd  21903  psrbaglefi  21958  cnrest2  23326  cnprest  23329  cnprest2  23330  lmss  23338  isfildlem  23897  isfcls  24049  elutop  24273  metustel  24590  blval2  24602  dscopn  24613  iscau2  25319  causs  25340  ismbf  25670  ismbfcn  25671  iblcnlem  25831  limcdif  25918  limcres  25928  limcun  25937  dvres  25953  q1peqb  26196  ulmval  26420  ulmres  26428  chpchtsum  27260  dchrisum0lem1  27557  elmade  27927  axcontlem5  29115  iswlkg  29760  issiga  34370  ismeas  34457  elcarsg  34563  cvmlift3lem4  35636  msrrcl  35857  brcolinear2  36372  topfneec  36679  bj-epelg  37517  cnpwstotbnd  38260  ismtyima  38266  ismndo2  38337  isrngo  38360  lshpkr  39705  fimgmcyc  43116  elrfi  43239  traxext  45517  climf  46162  climf2  46204  isupwlkg  48723