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  3825  rmob  3842  elpr2g  4608  oteqex  5456  epelg  5533  eqbrrdva  5826  relbrcnvg  6072  ordsucuniel  7776  ordsucun  7777  xpord2pred  8097  brtpos2  8184  eceqoveq  8771  elpmg  8792  elfi2  9329  brwdom  9484  brwdomn0  9486  rankr1c  9745  r1pwcl  9771  ttukeylem1  10431  fpwwe2lem8  10561  eltskm  10766  recmulnq  10887  clim  15429  rlim  15430  lo1o1  15467  o1lo1  15472  o1lo12  15473  rlimresb  15500  lo1eq  15503  rlimeq  15504  isercolllem2  15601  caucvgb  15615  saddisj  16404  sadadd  16406  sadass  16410  bitsshft  16414  smupvallem  16422  smumul  16432  catpropd  17644  isssc  17756  issubc  17771  funcres2b  17833  funcres2c  17839  sgrppropd  18668  mndpropd  18696  issubg3  19086  resghm2b  19175  resscntz  19274  elsymgbas  19315  odmulg  19497  dmdprd  19941  dprdw  19953  subgdmdprd  19977  lmodprop2d  20887  lssacs  20930  prmirred  21441  lindfmm  21794  lsslindf  21797  islinds3  21801  assapropd  21839  psrbaglefi  21894  cnrest2  23242  cnprest  23245  cnprest2  23246  lmss  23254  isfildlem  23813  isfcls  23965  elutop  24189  metustel  24506  blval2  24518  dscopn  24529  iscau2  25245  causs  25266  ismbf  25597  ismbfcn  25598  iblcnlem  25758  limcdif  25845  limcres  25855  limcun  25864  dvres  25880  q1peqb  26129  ulmval  26357  ulmres  26365  chpchtsum  27198  dchrisum0lem1  27495  elmade  27865  axcontlem5  29053  iswlkg  29699  issiga  34289  ismeas  34376  elcarsg  34482  cvmlift3lem4  35535  msrrcl  35756  brcolinear2  36271  topfneec  36568  bj-epelg  37310  cnpwstotbnd  38042  ismtyima  38048  ismndo2  38119  isrngo  38142  lshpkr  39487  fimgmcyc  42898  elrfi  43045  traxext  45327  climf  45976  climf2  46018  isupwlkg  48491