Theorem pm5.21ndd 380

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 205

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 206

This theorem is referenced by:  pm5.21nd  800  sbcrext  3832  rmob  3849  elpr2g  4615  oteqex  5462  epelg  5543  eqbrrdva  5830  relbrcnvg  6062  ordsucuniel  7764  ordsucun  7765  xpord2pred  8082  brtpos2  8168  eceqoveq  8768  elpmg  8788  elfi2  9359  brwdom  9512  brwdomn0  9514  rankr1c  9766  r1pwcl  9792  ttukeylem1  10454  fpwwe2lem8  10583  eltskm  10788  recmulnq  10909  clim  15388  rlim  15389  lo1o1  15426  o1lo1  15431  o1lo12  15432  rlimresb  15459  lo1eq  15462  rlimeq  15463  isercolllem2  15562  caucvgb  15576  saddisj  16356  sadadd  16358  sadass  16362  bitsshft  16366  smupvallem  16374  smumul  16384  catpropd  17603  isssc  17717  issubc  17735  funcres2b  17797  funcres2c  17802  mndpropd  18595  issubg3  18960  resghm2b  19040  resscntz  19126  elsymgbas  19169  odmulg  19352  dmdprd  19791  dprdw  19803  subgdmdprd  19827  lmodprop2d  20441  lssacs  20485  prmirred  20932  lindfmm  21270  lsslindf  21273  islinds3  21277  assapropd  21312  psrbaglefi  21371  psrbaglefiOLD  21372  cnrest2  22674  cnprest  22677  cnprest2  22678  lmss  22686  isfildlem  23245  isfcls  23397  elutop  23622  metustel  23943  blval2  23955  dscopn  23966  iscau2  24678  causs  24699  ismbf  25029  ismbfcn  25030  iblcnlem  25190  limcdif  25277  limcres  25287  limcun  25296  dvres  25312  q1peqb  25556  ulmval  25776  ulmres  25784  chpchtsum  26604  dchrisum0lem1  26901  elmade  27240  axcontlem5  27980  iswlkg  28624  issiga  32800  ismeas  32887  elcarsg  32994  cvmlift3lem4  34003  msrrcl  34224  brcolinear2  34719  topfneec  34903  bj-epelg  35612  cnpwstotbnd  36329  ismtyima  36335  ismndo2  36406  isrngo  36429  lshpkr  37652  elrfi  41075  climf  43983  climf2  44027  isupwlkg  46159