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  3824  rmob  3841  elpr2g  4602  oteqex  5440  epelg  5517  eqbrrdva  5809  relbrcnvg  6054  ordsucuniel  7754  ordsucun  7755  xpord2pred  8075  brtpos2  8162  eceqoveq  8746  elpmg  8767  elfi2  9298  brwdom  9453  brwdomn0  9455  rankr1c  9711  r1pwcl  9737  ttukeylem1  10397  fpwwe2lem8  10526  eltskm  10731  recmulnq  10852  clim  15398  rlim  15399  lo1o1  15436  o1lo1  15441  o1lo12  15442  rlimresb  15469  lo1eq  15472  rlimeq  15473  isercolllem2  15570  caucvgb  15584  saddisj  16373  sadadd  16375  sadass  16379  bitsshft  16383  smupvallem  16391  smumul  16401  catpropd  17612  isssc  17724  issubc  17739  funcres2b  17801  funcres2c  17807  sgrppropd  18636  mndpropd  18664  issubg3  19054  resghm2b  19144  resscntz  19243  elsymgbas  19284  odmulg  19466  dmdprd  19910  dprdw  19922  subgdmdprd  19946  lmodprop2d  20855  lssacs  20898  prmirred  21409  lindfmm  21762  lsslindf  21765  islinds3  21769  assapropd  21807  psrbaglefi  21861  cnrest2  23199  cnprest  23202  cnprest2  23203  lmss  23211  isfildlem  23770  isfcls  23922  elutop  24146  metustel  24463  blval2  24475  dscopn  24486  iscau2  25202  causs  25223  ismbf  25554  ismbfcn  25555  iblcnlem  25715  limcdif  25802  limcres  25812  limcun  25821  dvres  25837  q1peqb  26086  ulmval  26314  ulmres  26322  chpchtsum  27155  dchrisum0lem1  27452  elmade  27810  axcontlem5  28944  iswlkg  29590  issiga  34120  ismeas  34207  elcarsg  34313  cvmlift3lem4  35354  msrrcl  35575  brcolinear2  36091  topfneec  36388  bj-epelg  37101  cnpwstotbnd  37836  ismtyima  37842  ismndo2  37913  isrngo  37936  lshpkr  39155  fimgmcyc  42566  elrfi  42726  traxext  45009  climf  45661  climf2  45703  isupwlkg  48167