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  18818  mndpropd  18846  issubg3  19242  resghm2b  19335  resscntz  19434  elsymgbas  19475  odmulg  19657  dmdprd  20101  dprdw  20113  subgdmdprd  20137  lmodprop2d  21082  lssacs  21125  prmirred  21661  lindfmm  22014  lsslindf  22017  islinds3  22021  assapropd  22058  psrbaglefi  22113  cnrest2  23480  cnprest  23483  cnprest2  23484  lmss  23492  isfildlem  24051  isfcls  24203  elutop  24427  metustel  24744  blval2  24756  dscopn  24767  iscau2  25473  causs  25494  ismbf  25824  ismbfcn  25825  iblcnlem  25985  limcdif  26072  limcres  26082  limcun  26091  dvres  26107  q1peqb  26350  ulmval  26580  ulmres  26588  chpchtsum  27420  dchrisum0lem1  27717  elmade  28087  axcontlem5  29355  iswlkg  30000  issiga  34533  ismeas  34621  elcarsg  34727  cvmlift3lem4  35835  msrrcl  36056  brcolinear2  36571  topfneec  36907  bj-epelg  37745  cnpwstotbnd  38489  ismtyima  38495  ismndo2  38566  isrngo  38589  lshpkr  39932  fimgmcyc  43343  elrfi  43466  traxext  45727  climf  46379  climf2  46421  isupwlkg  48943