Theorem pm5.21ndd 369

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 148	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4		pm5.21ndd.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜓))
5	4	con3d 148	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6		pm5.21im 364	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 70	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 170	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

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

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 197

This theorem is referenced by:  pm5.21nd  941  sbcrext  3511  rmob  3529  oteqex  4964  epelg  5030  eqbrrdva  5291  relbrcnvg  5504  ordsucuniel  7024  ordsucun  7025  brtpos2  7358  eceqoveq  7853  elpmg  7873  elfi2  8320  brwdom  8472  brwdomn0  8474  rankr1c  8684  r1pwcl  8710  ttukeylem1  9331  fpwwe2lem9  9460  eltskm  9665  recmulnq  9786  clim  14225  rlim  14226  lo1o1  14263  o1lo1  14268  o1lo12  14269  rlimresb  14296  lo1eq  14299  rlimeq  14300  isercolllem2  14396  caucvgb  14410  saddisj  15187  sadadd  15189  sadass  15193  bitsshft  15197  smupvallem  15205  smumul  15215  catpropd  16369  isssc  16480  issubc  16495  funcres2b  16557  funcres2c  16561  mndpropd  17316  issubg3  17612  resghm2b  17678  resscntz  17764  elsymgbas  17802  odmulg  17973  dmdprd  18397  dprdw  18409  subgdmdprd  18433  lmodprop2d  18925  lssacs  18967  assapropd  19327  psrbaglefi  19372  prmirred  19843  lindfmm  20166  lsslindf  20169  islinds3  20173  cnrest2  21090  cnprest  21093  cnprest2  21094  lmss  21102  isfildlem  21661  isfcls  21813  elutop  22037  metustel  22355  blval2  22367  dscopn  22378  iscau2  23075  causs  23096  ismbf  23397  ismbfcn  23398  iblcnlem  23555  limcdif  23640  limcres  23650  limcun  23659  dvres  23675  q1peqb  23914  ulmval  24134  ulmres  24142  chpchtsum  24944  dchrisum0lem1  25205  axcontlem5  25848  iswlkg  26509  issiga  30174  ismeas  30262  elcarsg  30367  cvmlift3lem4  31304  msrrcl  31440  brcolinear2  32165  topfneec  32350  cnpwstotbnd  33596  ismtyima  33602  ismndo2  33673  isrngo  33696  lshpkr  34404  elrfi  37257  climf  39854  climf2  39898  isupwlkg  41718