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  3839  rmob  3856  elpr2g  4618  oteqex  5463  epelg  5542  eqbrrdva  5836  relbrcnvg  6079  ordsucuniel  7802  ordsucun  7803  xpord2pred  8127  brtpos2  8214  eceqoveq  8798  elpmg  8819  elfi2  9372  brwdom  9527  brwdomn0  9529  rankr1c  9781  r1pwcl  9807  ttukeylem1  10469  fpwwe2lem8  10598  eltskm  10803  recmulnq  10924  clim  15467  rlim  15468  lo1o1  15505  o1lo1  15510  o1lo12  15511  rlimresb  15538  lo1eq  15541  rlimeq  15542  isercolllem2  15639  caucvgb  15653  saddisj  16442  sadadd  16444  sadass  16448  bitsshft  16452  smupvallem  16460  smumul  16470  catpropd  17677  isssc  17789  issubc  17804  funcres2b  17866  funcres2c  17872  sgrppropd  18665  mndpropd  18693  issubg3  19083  resghm2b  19173  resscntz  19272  elsymgbas  19311  odmulg  19493  dmdprd  19937  dprdw  19949  subgdmdprd  19973  lmodprop2d  20837  lssacs  20880  prmirred  21391  lindfmm  21743  lsslindf  21746  islinds3  21750  assapropd  21788  psrbaglefi  21842  cnrest2  23180  cnprest  23183  cnprest2  23184  lmss  23192  isfildlem  23751  isfcls  23903  elutop  24128  metustel  24445  blval2  24457  dscopn  24468  iscau2  25184  causs  25205  ismbf  25536  ismbfcn  25537  iblcnlem  25697  limcdif  25784  limcres  25794  limcun  25803  dvres  25819  q1peqb  26068  ulmval  26296  ulmres  26304  chpchtsum  27137  dchrisum0lem1  27434  elmade  27786  axcontlem5  28902  iswlkg  29548  issiga  34109  ismeas  34196  elcarsg  34303  cvmlift3lem4  35316  msrrcl  35537  brcolinear2  36053  topfneec  36350  bj-epelg  37063  cnpwstotbnd  37798  ismtyima  37804  ismndo2  37875  isrngo  37898  lshpkr  39117  fimgmcyc  42529  elrfi  42689  traxext  44974  climf  45627  climf2  45671  isupwlkg  48129