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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.21nd  814  sbcrext  3829  rmob  3846  elpr2g  4620  oteqex  5488  epelg  5567  eqbrrdva  5860  relbrcnvg  6112  ordsucuniel  7829  ordsucun  7830  xpord2pred  8150  brtpos2  8237  eceqoveq  8829  elpmg  8849  elfi2  9384  brwdom  9539  brwdomn0  9541  rankr1c  9803  r1pwcl  9829  ttukeylem1  10511  fpwwe2lem8  10641  eltskm  10846  recmulnq  10967  clim  15571  rlim  15572  lo1o1  15609  o1lo1  15614  o1lo12  15615  rlimresb  15642  lo1eq  15645  rlimeq  15646  isercolllem2  15743  caucvgb  15757  saddisj  16548  sadadd  16550  sadass  16554  bitsshft  16558  smupvallem  16566  smumul  16576  catpropd  17790  isssc  17902  issubc  17917  funcres2b  17979  funcres2c  17985  sgrppropd  18814  mndpropd  18842  issubg3  19236  resghm2b  19329  resscntz  19428  elsymgbas  19469  odmulg  19651  dmdprd  20095  dprdw  20107  subgdmdprd  20131  lmodprop2d  21075  lssacs  21118  prmirred  21654  lindfmm  22007  lsslindf  22010  islinds3  22014  assapropd  22051  psrbaglefi  22106  cnrest2  23473  cnprest  23476  cnprest2  23477  lmss  23485  isfildlem  24044  isfcls  24196  elutop  24420  metustel  24737  blval2  24749  dscopn  24760  iscau2  25466  causs  25487  ismbf  25817  ismbfcn  25818  iblcnlem  25978  limcdif  26065  limcres  26075  limcun  26084  dvres  26100  q1peqb  26343  ulmval  26573  ulmres  26581  chpchtsum  27413  dchrisum0lem1  27710  elmade  28080  axcontlem5  29348  iswlkg  29993  issiga  34526  ismeas  34613  elcarsg  34719  cvmlift3lem4  35827  msrrcl  36048  brcolinear2  36563  topfneec  36899  bj-epelg  37737  cnpwstotbnd  38481  ismtyima  38487  ismndo2  38558  isrngo  38581  lshpkr  39924  fimgmcyc  43335  elrfi  43458  traxext  45719  climf  46371  climf2  46413  isupwlkg  48935