Theorem pm5.21ndd 379

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

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

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 207

This theorem is referenced by:  pm5.21nd  802  sbcrext  3873  rmob  3890  elpr2g  4651  oteqex  5505  epelg  5585  eqbrrdva  5880  relbrcnvg  6123  ordsucuniel  7844  ordsucun  7845  xpord2pred  8170  brtpos2  8257  eceqoveq  8862  elpmg  8883  elfi2  9454  brwdom  9607  brwdomn0  9609  rankr1c  9861  r1pwcl  9887  ttukeylem1  10549  fpwwe2lem8  10678  eltskm  10883  recmulnq  11004  clim  15530  rlim  15531  lo1o1  15568  o1lo1  15573  o1lo12  15574  rlimresb  15601  lo1eq  15604  rlimeq  15605  isercolllem2  15702  caucvgb  15716  saddisj  16502  sadadd  16504  sadass  16508  bitsshft  16512  smupvallem  16520  smumul  16530  catpropd  17752  isssc  17864  issubc  17880  funcres2b  17942  funcres2c  17948  sgrppropd  18744  mndpropd  18772  issubg3  19162  resghm2b  19252  resscntz  19351  elsymgbas  19391  odmulg  19574  dmdprd  20018  dprdw  20030  subgdmdprd  20054  lmodprop2d  20922  lssacs  20965  prmirred  21485  lindfmm  21847  lsslindf  21850  islinds3  21854  assapropd  21892  psrbaglefi  21946  cnrest2  23294  cnprest  23297  cnprest2  23298  lmss  23306  isfildlem  23865  isfcls  24017  elutop  24242  metustel  24563  blval2  24575  dscopn  24586  iscau2  25311  causs  25332  ismbf  25663  ismbfcn  25664  iblcnlem  25824  limcdif  25911  limcres  25921  limcun  25930  dvres  25946  q1peqb  26195  ulmval  26423  ulmres  26431  chpchtsum  27263  dchrisum0lem1  27560  elmade  27906  axcontlem5  28983  iswlkg  29631  issiga  34113  ismeas  34200  elcarsg  34307  cvmlift3lem4  35327  msrrcl  35548  brcolinear2  36059  topfneec  36356  bj-epelg  37069  cnpwstotbnd  37804  ismtyima  37810  ismndo2  37881  isrngo  37904  lshpkr  39118  fimgmcyc  42544  elrfi  42705  traxext  44994  climf  45637  climf2  45681  isupwlkg  48053