Theorem pm5.21ndd 384

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 378	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 182	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  pm5.21nd  802  sbcrext  3776  rmob  3793  elpr2g  4555  oteqex  5372  epelg  5450  eqbrrdva  5727  relbrcnvg  5962  ordsucuniel  7592  ordsucun  7593  brtpos2  7963  eceqoveq  8493  elpmg  8513  elfi2  9019  brwdom  9172  brwdomn0  9174  rankr1c  9420  r1pwcl  9446  ttukeylem1  10106  fpwwe2lem8  10235  eltskm  10440  recmulnq  10561  clim  15038  rlim  15039  lo1o1  15076  o1lo1  15081  o1lo12  15082  rlimresb  15109  lo1eq  15112  rlimeq  15113  isercolllem2  15212  caucvgb  15226  saddisj  16005  sadadd  16007  sadass  16011  bitsshft  16015  smupvallem  16023  smumul  16033  catpropd  17184  isssc  17297  issubc  17313  funcres2b  17375  funcres2c  17380  mndpropd  18170  issubg3  18533  resghm2b  18612  resscntz  18698  elsymgbas  18738  odmulg  18919  dmdprd  19357  dprdw  19369  subgdmdprd  19393  lmodprop2d  19933  lssacs  19976  prmirred  20433  lindfmm  20761  lsslindf  20764  islinds3  20768  assapropd  20803  psrbaglefi  20863  psrbaglefiOLD  20864  cnrest2  22155  cnprest  22158  cnprest2  22159  lmss  22167  isfildlem  22726  isfcls  22878  elutop  23103  metustel  23420  blval2  23432  dscopn  23443  iscau2  24146  causs  24167  ismbf  24497  ismbfcn  24498  iblcnlem  24658  limcdif  24745  limcres  24755  limcun  24764  dvres  24780  q1peqb  25024  ulmval  25244  ulmres  25252  chpchtsum  26072  dchrisum0lem1  26369  axcontlem5  27031  iswlkg  27673  issiga  31764  ismeas  31851  elcarsg  31956  cvmlift3lem4  32969  msrrcl  33190  xpord2pred  33480  elmade  33745  brcolinear2  34054  topfneec  34238  bj-epelg  34932  cnpwstotbnd  35649  ismtyima  35655  ismndo2  35726  isrngo  35749  lshpkr  36825  elrfi  40171  climf  42792  climf2  42836  isupwlkg  44926