Theorem pm5.21ndd 383

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 155	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4		pm5.21ndd.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜓))
5	4	con3d 155	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6		pm5.21im 377	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 181	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  800  sbcrext  3858  rmob  3876  oteqex  5392  epelg  5468  epelgOLD  5469  eqbrrdva  5742  relbrcnvg  5970  ordsucuniel  7541  ordsucun  7542  brtpos2  7900  eceqoveq  8404  elpmg  8424  elfi2  8880  brwdom  9033  brwdomn0  9035  rankr1c  9252  r1pwcl  9278  ttukeylem1  9933  fpwwe2lem9  10062  eltskm  10267  recmulnq  10388  clim  14853  rlim  14854  lo1o1  14891  o1lo1  14896  o1lo12  14897  rlimresb  14924  lo1eq  14927  rlimeq  14928  isercolllem2  15024  caucvgb  15038  saddisj  15816  sadadd  15818  sadass  15822  bitsshft  15826  smupvallem  15834  smumul  15844  catpropd  16981  isssc  17092  issubc  17107  funcres2b  17169  funcres2c  17173  mndpropd  17938  issubg3  18299  resghm2b  18378  resscntz  18464  elsymgbas  18504  odmulg  18685  dmdprd  19122  dprdw  19134  subgdmdprd  19158  lmodprop2d  19698  lssacs  19741  assapropd  20103  psrbaglefi  20154  prmirred  20644  lindfmm  20973  lsslindf  20976  islinds3  20980  cnrest2  21896  cnprest  21899  cnprest2  21900  lmss  21908  isfildlem  22467  isfcls  22619  elutop  22844  metustel  23162  blval2  23174  dscopn  23185  iscau2  23882  causs  23903  ismbf  24231  ismbfcn  24232  iblcnlem  24391  limcdif  24476  limcres  24486  limcun  24495  dvres  24511  q1peqb  24750  ulmval  24970  ulmres  24978  chpchtsum  25797  dchrisum0lem1  26094  axcontlem5  26756  iswlkg  27397  issiga  31373  ismeas  31460  elcarsg  31565  cvmlift3lem4  32571  msrrcl  32792  brcolinear2  33521  topfneec  33705  bj-epelg  34362  cnpwstotbnd  35077  ismtyima  35083  ismndo2  35154  isrngo  35177  lshpkr  36255  elrfi  39298  climf  41910  climf2  41954  isupwlkg  44019