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 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.21nd  814  sbcrext  3820  rmob  3837  elpr2g  4610  oteqex  5472  epelg  5552  eqbrrdva  5847  relbrcnvg  6099  ordsucuniel  7824  ordsucun  7825  xpord2pred  8146  brtpos2  8233  eceqoveq  8827  elpmg  8847  elfi2  9390  brwdom  9545  brwdomn0  9547  rankr1c  9811  r1pwcl  9842  ttukeylem1  10568  fpwwe2lem8  10704  eltskm  10909  recmulnq  11030  clim  15641  rlim  15642  lo1o1  15679  o1lo1  15684  o1lo12  15685  rlimresb  15712  lo1eq  15715  rlimeq  15716  isercolllem2  15813  caucvgb  15827  saddisj  16615  sadadd  16617  sadass  16621  bitsshft  16625  smupvallem  16633  smumul  16643  catpropd  17863  isssc  17975  issubc  17990  funcres2b  18052  funcres2c  18058  sgrppropd  18900  mndpropd  18931  issubg3  19335  resghm2b  19428  resscntz  19527  elsymgbas  19568  odmulg  19750  dmdprd  20194  dprdw  20206  subgdmdprd  20230  lmodprop2d  21179  lssacs  21222  prmirred  21760  lindfmm  22113  lsslindf  22116  islinds3  22120  assapropd  22159  psrbaglefi  22214  cnrest2  23584  cnprest  23587  cnprest2  23588  lmss  23596  isfildlem  24156  isfcls  24308  elutop  24532  metustel  24849  blval2  24861  dscopn  24872  iscau2  25578  causs  25599  ismbf  25929  ismbfcn  25930  iblcnlem  26089  limcdif  26176  limcres  26186  limcun  26195  dvres  26211  q1peqb  26454  ulmval  26689  ulmres  26697  chpchtsum  27528  dchrisum0lem1  27825  elmade  28225  axcontlem5  29528  iswlkg  30176  issiga  34726  ismeas  34814  elcarsg  34920  cvmlift3lem4  36056  msrrcl  36277  brcolinear2  36793  topfneec  37113  bj-epelg  37951  cnpwstotbnd  38699  ismtyima  38705  ismndo2  38776  isrngo  38799  lshpkr  40142  fimgmcyc  43560  elrfi  43658  traxext  45919  climf  46578  climf2  46620  isupwlkg  49179