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  801  sbcrext  3820  rmob  3837  elpr2g  4601  oteqex  5443  epelg  5520  eqbrrdva  5813  relbrcnvg  6058  ordsucuniel  7760  ordsucun  7761  xpord2pred  8081  brtpos2  8168  eceqoveq  8752  elpmg  8773  elfi2  9305  brwdom  9460  brwdomn0  9462  rankr1c  9721  r1pwcl  9747  ttukeylem1  10407  fpwwe2lem8  10536  eltskm  10741  recmulnq  10862  clim  15403  rlim  15404  lo1o1  15441  o1lo1  15446  o1lo12  15447  rlimresb  15474  lo1eq  15477  rlimeq  15478  isercolllem2  15575  caucvgb  15589  saddisj  16378  sadadd  16380  sadass  16384  bitsshft  16388  smupvallem  16396  smumul  16406  catpropd  17617  isssc  17729  issubc  17744  funcres2b  17806  funcres2c  17812  sgrppropd  18641  mndpropd  18669  issubg3  19059  resghm2b  19148  resscntz  19247  elsymgbas  19288  odmulg  19470  dmdprd  19914  dprdw  19926  subgdmdprd  19950  lmodprop2d  20859  lssacs  20902  prmirred  21413  lindfmm  21766  lsslindf  21769  islinds3  21773  assapropd  21811  psrbaglefi  21865  cnrest2  23202  cnprest  23205  cnprest2  23206  lmss  23214  isfildlem  23773  isfcls  23925  elutop  24149  metustel  24466  blval2  24478  dscopn  24489  iscau2  25205  causs  25226  ismbf  25557  ismbfcn  25558  iblcnlem  25718  limcdif  25805  limcres  25815  limcun  25824  dvres  25840  q1peqb  26089  ulmval  26317  ulmres  26325  chpchtsum  27158  dchrisum0lem1  27455  elmade  27813  axcontlem5  28948  iswlkg  29594  issiga  34146  ismeas  34233  elcarsg  34339  cvmlift3lem4  35387  msrrcl  35608  brcolinear2  36123  topfneec  36420  bj-epelg  37133  cnpwstotbnd  37857  ismtyima  37863  ismndo2  37934  isrngo  37957  lshpkr  39236  fimgmcyc  42652  elrfi  42811  traxext  45094  climf  45746  climf2  45788  isupwlkg  48261