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  3824  rmob  3841  elpr2g  4610  oteqex  5477  epelg  5557  eqbrrdva  5855  relbrcnvg  6114  ordsucuniel  7862  ordsucun  7863  xpord2pred  8192  brtpos2  8280  eceqoveq  8874  elpmg  8894  elfi2  9436  brwdom  9591  brwdomn0  9593  rankr1c  9860  r1pwcl  9891  ttukeylem1  10617  fpwwe2lem8  10753  eltskm  10958  recmulnq  11079  clim  15693  rlim  15694  lo1o1  15731  o1lo1  15736  o1lo12  15737  rlimresb  15764  lo1eq  15767  rlimeq  15768  isercolllem2  15865  caucvgb  15879  saddisj  16667  sadadd  16669  sadass  16673  bitsshft  16677  smupvallem  16685  smumul  16695  catpropd  17915  isssc  18027  issubc  18042  funcres2b  18104  funcres2c  18110  sgrppropd  18952  mndpropd  18983  issubg3  19387  resghm2b  19480  resscntz  19580  elsymgbas  19621  odmulg  19803  dmdprd  20247  dprdw  20259  subgdmdprd  20283  lmodprop2d  21232  lssacs  21275  prmirred  21813  lindfmm  22166  lsslindf  22169  islinds3  22173  assapropd  22212  psrbaglefi  22267  cnrest2  23637  cnprest  23640  cnprest2  23641  lmss  23649  isfildlem  24209  isfcls  24361  elutop  24585  metustel  24902  blval2  24914  dscopn  24925  iscau2  25631  causs  25652  ismbf  25982  ismbfcn  25983  iblcnlem  26142  limcdif  26229  limcres  26239  limcun  26248  dvres  26264  q1peqb  26507  ulmval  26740  ulmres  26748  chpchtsum  27579  dchrisum0lem1  27876  elmade  28276  axcontlem5  29579  iswlkg  30227  issiga  34827  ismeas  34915  elcarsg  35020  cvmlift3lem4  36267  msrrcl  36488  brcolinear2  37014  topfneec  37334  bj-epelg  38187  cnpwstotbnd  38934  ismtyima  38940  ismndo2  39011  isrngo  39034  lshpkr  40377  fimgmcyc  43802  elrfi  43909  traxext  46173  climf  46849  climf2  46891  isupwlkg  49450