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  801  sbcrext  3827  rmob  3844  elpr2g  4605  oteqex  5447  epelg  5524  eqbrrdva  5816  relbrcnvg  6060  ordsucuniel  7763  ordsucun  7764  xpord2pred  8085  brtpos2  8172  eceqoveq  8756  elpmg  8777  elfi2  9323  brwdom  9478  brwdomn0  9480  rankr1c  9736  r1pwcl  9762  ttukeylem1  10422  fpwwe2lem8  10551  eltskm  10756  recmulnq  10877  clim  15419  rlim  15420  lo1o1  15457  o1lo1  15462  o1lo12  15463  rlimresb  15490  lo1eq  15493  rlimeq  15494  isercolllem2  15591  caucvgb  15605  saddisj  16394  sadadd  16396  sadass  16400  bitsshft  16404  smupvallem  16412  smumul  16422  catpropd  17633  isssc  17745  issubc  17760  funcres2b  17822  funcres2c  17828  sgrppropd  18623  mndpropd  18651  issubg3  19041  resghm2b  19131  resscntz  19230  elsymgbas  19271  odmulg  19453  dmdprd  19897  dprdw  19909  subgdmdprd  19933  lmodprop2d  20845  lssacs  20888  prmirred  21399  lindfmm  21752  lsslindf  21755  islinds3  21759  assapropd  21797  psrbaglefi  21851  cnrest2  23189  cnprest  23192  cnprest2  23193  lmss  23201  isfildlem  23760  isfcls  23912  elutop  24137  metustel  24454  blval2  24466  dscopn  24477  iscau2  25193  causs  25214  ismbf  25545  ismbfcn  25546  iblcnlem  25706  limcdif  25793  limcres  25803  limcun  25812  dvres  25828  q1peqb  26077  ulmval  26305  ulmres  26313  chpchtsum  27146  dchrisum0lem1  27443  elmade  27799  axcontlem5  28931  iswlkg  29577  issiga  34078  ismeas  34165  elcarsg  34272  cvmlift3lem4  35294  msrrcl  35515  brcolinear2  36031  topfneec  36328  bj-epelg  37041  cnpwstotbnd  37776  ismtyima  37782  ismndo2  37853  isrngo  37876  lshpkr  39095  fimgmcyc  42507  elrfi  42667  traxext  44951  climf  45604  climf2  45648  isupwlkg  48122