Theorem pm5.21ndd 382

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 153	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4		pm5.21ndd.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜓))
5	4	con3d 153	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃))
6		pm5.21im 377	. . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃)))
7	3, 5, 6	syl6c 71	. 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃)))
8	1, 7	pm2.61d 181	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  813  sbcrext  3827  rmob  3844  elpr2g  4616  oteqex  5485  epelg  5564  eqbrrdva  5857  relbrcnvg  6109  ordsucuniel  7821  ordsucun  7822  xpord2pred  8142  brtpos2  8229  eceqoveq  8821  elpmg  8841  elfi2  9375  brwdom  9530  brwdomn0  9532  rankr1c  9794  r1pwcl  9820  ttukeylem1  10494  fpwwe2lem8  10624  eltskm  10829  recmulnq  10950  clim  15547  rlim  15548  lo1o1  15585  o1lo1  15590  o1lo12  15591  rlimresb  15618  lo1eq  15621  rlimeq  15622  isercolllem2  15719  caucvgb  15733  saddisj  16524  sadadd  16526  sadass  16530  bitsshft  16534  smupvallem  16542  smumul  16552  catpropd  17766  isssc  17878  issubc  17893  funcres2b  17955  funcres2c  17961  sgrppropd  18790  mndpropd  18818  issubg3  19212  resghm2b  19305  resscntz  19404  elsymgbas  19445  odmulg  19627  dmdprd  20071  dprdw  20083  subgdmdprd  20107  lmodprop2d  21026  lssacs  21069  prmirred  21605  lindfmm  21958  lsslindf  21961  islinds3  21965  assapropd  22002  psrbaglefi  22057  cnrest2  23424  cnprest  23427  cnprest2  23428  lmss  23436  isfildlem  23995  isfcls  24147  elutop  24371  metustel  24688  blval2  24700  dscopn  24711  iscau2  25417  causs  25438  ismbf  25768  ismbfcn  25769  iblcnlem  25929  limcdif  26016  limcres  26026  limcun  26035  dvres  26051  q1peqb  26294  ulmval  26524  ulmres  26532  chpchtsum  27364  dchrisum0lem1  27661  elmade  28031  axcontlem5  29299  iswlkg  29944  issiga  34483  ismeas  34570  elcarsg  34676  cvmlift3lem4  35795  msrrcl  36016  brcolinear2  36531  topfneec  36847  bj-epelg  37685  cnpwstotbnd  38429  ismtyima  38435  ismndo2  38506  isrngo  38529  lshpkr  39872  fimgmcyc  43285  elrfi  43408  traxext  45669  climf  46321  climf2  46363  isupwlkg  48885