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  802  sbcrext  3881  rmob  3898  elpr2g  4655  oteqex  5509  epelg  5589  eqbrrdva  5882  relbrcnvg  6125  ordsucuniel  7843  ordsucun  7844  xpord2pred  8168  brtpos2  8255  eceqoveq  8860  elpmg  8881  elfi2  9451  brwdom  9604  brwdomn0  9606  rankr1c  9858  r1pwcl  9884  ttukeylem1  10546  fpwwe2lem8  10675  eltskm  10880  recmulnq  11001  clim  15526  rlim  15527  lo1o1  15564  o1lo1  15569  o1lo12  15570  rlimresb  15597  lo1eq  15600  rlimeq  15601  isercolllem2  15698  caucvgb  15712  saddisj  16498  sadadd  16500  sadass  16504  bitsshft  16508  smupvallem  16516  smumul  16526  catpropd  17753  isssc  17867  issubc  17885  funcres2b  17947  funcres2c  17954  sgrppropd  18756  mndpropd  18784  issubg3  19174  resghm2b  19264  resscntz  19363  elsymgbas  19405  odmulg  19588  dmdprd  20032  dprdw  20044  subgdmdprd  20068  lmodprop2d  20938  lssacs  20982  prmirred  21502  lindfmm  21864  lsslindf  21867  islinds3  21871  assapropd  21909  psrbaglefi  21963  cnrest2  23309  cnprest  23312  cnprest2  23313  lmss  23321  isfildlem  23880  isfcls  24032  elutop  24257  metustel  24578  blval2  24590  dscopn  24601  iscau2  25324  causs  25345  ismbf  25676  ismbfcn  25677  iblcnlem  25838  limcdif  25925  limcres  25935  limcun  25944  dvres  25960  q1peqb  26209  ulmval  26437  ulmres  26445  chpchtsum  27277  dchrisum0lem1  27574  elmade  27920  axcontlem5  28997  iswlkg  29645  issiga  34092  ismeas  34179  elcarsg  34286  cvmlift3lem4  35306  msrrcl  35527  brcolinear2  36039  topfneec  36337  bj-epelg  37050  cnpwstotbnd  37783  ismtyima  37789  ismndo2  37860  isrngo  37883  lshpkr  39098  fimgmcyc  42520  elrfi  42681  traxext  44937  climf  45577  climf2  45621  isupwlkg  47980