Theorem pm5.21ndd 381

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

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

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 206

This theorem is referenced by:  pm5.21nd  799  sbcrext  3807  rmob  3824  elpr2g  4586  oteqex  5415  epelg  5497  eqbrrdva  5781  relbrcnvg  6016  ordsucuniel  7680  ordsucun  7681  brtpos2  8057  eceqoveq  8620  elpmg  8640  elfi2  9182  brwdom  9335  brwdomn0  9337  rankr1c  9588  r1pwcl  9614  ttukeylem1  10274  fpwwe2lem8  10403  eltskm  10608  recmulnq  10729  clim  15212  rlim  15213  lo1o1  15250  o1lo1  15255  o1lo12  15256  rlimresb  15283  lo1eq  15286  rlimeq  15287  isercolllem2  15386  caucvgb  15400  saddisj  16181  sadadd  16183  sadass  16187  bitsshft  16191  smupvallem  16199  smumul  16209  catpropd  17427  isssc  17541  issubc  17559  funcres2b  17621  funcres2c  17626  mndpropd  18419  issubg3  18782  resghm2b  18861  resscntz  18947  elsymgbas  18990  odmulg  19172  dmdprd  19610  dprdw  19622  subgdmdprd  19646  lmodprop2d  20194  lssacs  20238  prmirred  20705  lindfmm  21043  lsslindf  21046  islinds3  21050  assapropd  21085  psrbaglefi  21144  psrbaglefiOLD  21145  cnrest2  22446  cnprest  22449  cnprest2  22450  lmss  22458  isfildlem  23017  isfcls  23169  elutop  23394  metustel  23715  blval2  23727  dscopn  23738  iscau2  24450  causs  24471  ismbf  24801  ismbfcn  24802  iblcnlem  24962  limcdif  25049  limcres  25059  limcun  25068  dvres  25084  q1peqb  25328  ulmval  25548  ulmres  25556  chpchtsum  26376  dchrisum0lem1  26673  axcontlem5  27345  iswlkg  27989  issiga  32089  ismeas  32176  elcarsg  32281  cvmlift3lem4  33293  msrrcl  33514  xpord2pred  33801  elmade  34060  brcolinear2  34369  topfneec  34553  bj-epelg  35248  cnpwstotbnd  35964  ismtyima  35970  ismndo2  36041  isrngo  36064  lshpkr  37138  elrfi  40523  climf  43170  climf2  43214  isupwlkg  45310