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

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

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 208

This theorem is referenced by:  pm5.21nd  798  sbcrext  3790  rmob  3808  oteqex  5288  epelg  5361  epelgOLD  5362  eqbrrdva  5633  relbrcnvg  5851  ordsucuniel  7402  ordsucun  7403  brtpos2  7756  eceqoveq  8259  elpmg  8279  elfi2  8731  brwdom  8884  brwdomn0  8886  rankr1c  9103  r1pwcl  9129  ttukeylem1  9784  fpwwe2lem9  9913  eltskm  10118  recmulnq  10239  clim  14689  rlim  14690  lo1o1  14727  o1lo1  14732  o1lo12  14733  rlimresb  14760  lo1eq  14763  rlimeq  14764  isercolllem2  14860  caucvgb  14874  saddisj  15651  sadadd  15653  sadass  15657  bitsshft  15661  smupvallem  15669  smumul  15679  catpropd  16812  isssc  16923  issubc  16938  funcres2b  17000  funcres2c  17004  mndpropd  17759  issubg3  18055  resghm2b  18121  resscntz  18207  elsymgbas  18245  odmulg  18417  dmdprd  18841  dprdw  18853  subgdmdprd  18877  lmodprop2d  19390  lssacs  19433  assapropd  19793  psrbaglefi  19844  prmirred  20328  lindfmm  20657  lsslindf  20660  islinds3  20664  cnrest2  21582  cnprest  21585  cnprest2  21586  lmss  21594  isfildlem  22153  isfcls  22305  elutop  22529  metustel  22847  blval2  22859  dscopn  22870  iscau2  23567  causs  23588  ismbf  23916  ismbfcn  23917  iblcnlem  24076  limcdif  24161  limcres  24171  limcun  24180  dvres  24196  q1peqb  24435  ulmval  24655  ulmres  24663  chpchtsum  25481  dchrisum0lem1  25778  axcontlem5  26441  iswlkg  27082  issiga  30984  ismeas  31071  elcarsg  31176  cvmlift3lem4  32179  msrrcl  32400  brcolinear2  33130  topfneec  33314  cnpwstotbnd  34628  ismtyima  34634  ismndo2  34705  isrngo  34728  lshpkr  35805  elrfi  38797  climf  41466  climf2  41510  isupwlkg  43516