Theorem pm5.21ndd 378

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 373	. . 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  3868  rmob  3885  elpr2g  4657  oteqex  5506  epelg  5587  eqbrrdva  5876  relbrcnvg  6114  ordsucuniel  7833  ordsucun  7834  xpord2pred  8156  brtpos2  8244  eceqoveq  8847  elpmg  8868  elfi2  9445  brwdom  9598  brwdomn0  9600  rankr1c  9852  r1pwcl  9878  ttukeylem1  10540  fpwwe2lem8  10669  eltskm  10874  recmulnq  10995  clim  15478  rlim  15479  lo1o1  15516  o1lo1  15521  o1lo12  15522  rlimresb  15549  lo1eq  15552  rlimeq  15553  isercolllem2  15652  caucvgb  15666  saddisj  16447  sadadd  16449  sadass  16453  bitsshft  16457  smupvallem  16465  smumul  16475  catpropd  17696  isssc  17810  issubc  17828  funcres2b  17890  funcres2c  17897  sgrppropd  18698  mndpropd  18726  issubg3  19106  resghm2b  19195  resscntz  19291  elsymgbas  19335  odmulg  19518  dmdprd  19962  dprdw  19974  subgdmdprd  19998  lmodprop2d  20814  lssacs  20858  prmirred  21407  lindfmm  21768  lsslindf  21771  islinds3  21775  assapropd  21812  psrbaglefi  21872  psrbaglefiOLD  21873  cnrest2  23210  cnprest  23213  cnprest2  23214  lmss  23222  isfildlem  23781  isfcls  23933  elutop  24158  metustel  24479  blval2  24491  dscopn  24502  iscau2  25225  causs  25246  ismbf  25577  ismbfcn  25578  iblcnlem  25738  limcdif  25825  limcres  25835  limcun  25844  dvres  25860  q1peqb  26111  ulmval  26336  ulmres  26344  chpchtsum  27172  dchrisum0lem1  27469  elmade  27814  axcontlem5  28799  iswlkg  29447  issiga  33764  ismeas  33851  elcarsg  33958  cvmlift3lem4  34965  msrrcl  35186  brcolinear2  35687  topfneec  35872  bj-epelg  36580  cnpwstotbnd  37303  ismtyima  37309  ismndo2  37380  isrngo  37403  lshpkr  38621  elrfi  42145  climf  45039  climf2  45083  isupwlkg  47277