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  3823  rmob  3840  elpr2g  4613  oteqex  5481  epelg  5560  eqbrrdva  5853  relbrcnvg  6105  ordsucuniel  7824  ordsucun  7825  xpord2pred  8147  brtpos2  8234  eceqoveq  8826  elpmg  8846  elfi2  9388  brwdom  9543  brwdomn0  9545  rankr1c  9807  r1pwcl  9833  ttukeylem1  10515  fpwwe2lem8  10651  eltskm  10856  recmulnq  10977  clim  15585  rlim  15586  lo1o1  15623  o1lo1  15628  o1lo12  15629  rlimresb  15656  lo1eq  15659  rlimeq  15660  isercolllem2  15757  caucvgb  15771  saddisj  16561  sadadd  16563  sadass  16567  bitsshft  16571  smupvallem  16579  smumul  16589  catpropd  17803  isssc  17915  issubc  17930  funcres2b  17992  funcres2c  17998  sgrppropd  18839  mndpropd  18870  issubg3  19274  resghm2b  19367  resscntz  19466  elsymgbas  19507  odmulg  19689  dmdprd  20133  dprdw  20145  subgdmdprd  20169  lmodprop2d  21114  lssacs  21157  prmirred  21693  lindfmm  22046  lsslindf  22049  islinds3  22053  assapropd  22092  psrbaglefi  22147  cnrest2  23517  cnprest  23520  cnprest2  23521  lmss  23529  isfildlem  24089  isfcls  24241  elutop  24465  metustel  24782  blval2  24794  dscopn  24805  iscau2  25511  causs  25532  ismbf  25862  ismbfcn  25863  iblcnlem  26023  limcdif  26110  limcres  26120  limcun  26129  dvres  26145  q1peqb  26388  ulmval  26623  ulmres  26631  chpchtsum  27463  dchrisum0lem1  27760  elmade  28130  axcontlem5  29433  iswlkg  30081  issiga  34630  ismeas  34718  elcarsg  34824  cvmlift3lem4  35909  msrrcl  36130  brcolinear2  36646  topfneec  36982  bj-epelg  37820  cnpwstotbnd  38555  ismtyima  38561  ismndo2  38632  isrngo  38655  lshpkr  39998  fimgmcyc  43424  elrfi  43547  traxext  45808  climf  46460  climf2  46502  isupwlkg  49061