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  3821  rmob  3838  elpr2g  4599  oteqex  5437  epelg  5514  eqbrrdva  5806  relbrcnvg  6050  ordsucuniel  7748  ordsucun  7749  xpord2pred  8069  brtpos2  8156  eceqoveq  8740  elpmg  8761  elfi2  9292  brwdom  9447  brwdomn0  9449  rankr1c  9705  r1pwcl  9731  ttukeylem1  10391  fpwwe2lem8  10520  eltskm  10725  recmulnq  10846  clim  15388  rlim  15389  lo1o1  15426  o1lo1  15431  o1lo12  15432  rlimresb  15459  lo1eq  15462  rlimeq  15463  isercolllem2  15560  caucvgb  15574  saddisj  16363  sadadd  16365  sadass  16369  bitsshft  16373  smupvallem  16381  smumul  16391  catpropd  17602  isssc  17714  issubc  17729  funcres2b  17791  funcres2c  17797  sgrppropd  18592  mndpropd  18620  issubg3  19010  resghm2b  19100  resscntz  19199  elsymgbas  19240  odmulg  19422  dmdprd  19866  dprdw  19878  subgdmdprd  19902  lmodprop2d  20811  lssacs  20854  prmirred  21365  lindfmm  21718  lsslindf  21721  islinds3  21725  assapropd  21763  psrbaglefi  21817  cnrest2  23155  cnprest  23158  cnprest2  23159  lmss  23167  isfildlem  23726  isfcls  23878  elutop  24102  metustel  24419  blval2  24431  dscopn  24442  iscau2  25158  causs  25179  ismbf  25510  ismbfcn  25511  iblcnlem  25671  limcdif  25758  limcres  25768  limcun  25777  dvres  25793  q1peqb  26042  ulmval  26270  ulmres  26278  chpchtsum  27111  dchrisum0lem1  27408  elmade  27766  axcontlem5  28900  iswlkg  29546  issiga  34093  ismeas  34180  elcarsg  34286  cvmlift3lem4  35312  msrrcl  35533  brcolinear2  36049  topfneec  36346  bj-epelg  37059  cnpwstotbnd  37794  ismtyima  37800  ismndo2  37871  isrngo  37894  lshpkr  39113  fimgmcyc  42524  elrfi  42684  traxext  44967  climf  45619  climf2  45661  isupwlkg  48135