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  798  sbcrext  3802  rmob  3819  elpr2g  4582  oteqex  5408  epelg  5487  eqbrrdva  5767  relbrcnvg  6002  ordsucuniel  7646  ordsucun  7647  brtpos2  8019  eceqoveq  8569  elpmg  8589  elfi2  9103  brwdom  9256  brwdomn0  9258  rankr1c  9510  r1pwcl  9536  ttukeylem1  10196  fpwwe2lem8  10325  eltskm  10530  recmulnq  10651  clim  15131  rlim  15132  lo1o1  15169  o1lo1  15174  o1lo12  15175  rlimresb  15202  lo1eq  15205  rlimeq  15206  isercolllem2  15305  caucvgb  15319  saddisj  16100  sadadd  16102  sadass  16106  bitsshft  16110  smupvallem  16118  smumul  16128  catpropd  17335  isssc  17449  issubc  17466  funcres2b  17528  funcres2c  17533  mndpropd  18325  issubg3  18688  resghm2b  18767  resscntz  18853  elsymgbas  18896  odmulg  19078  dmdprd  19516  dprdw  19528  subgdmdprd  19552  lmodprop2d  20100  lssacs  20144  prmirred  20608  lindfmm  20944  lsslindf  20947  islinds3  20951  assapropd  20986  psrbaglefi  21045  psrbaglefiOLD  21046  cnrest2  22345  cnprest  22348  cnprest2  22349  lmss  22357  isfildlem  22916  isfcls  23068  elutop  23293  metustel  23612  blval2  23624  dscopn  23635  iscau2  24346  causs  24367  ismbf  24697  ismbfcn  24698  iblcnlem  24858  limcdif  24945  limcres  24955  limcun  24964  dvres  24980  q1peqb  25224  ulmval  25444  ulmres  25452  chpchtsum  26272  dchrisum0lem1  26569  axcontlem5  27239  iswlkg  27883  issiga  31980  ismeas  32067  elcarsg  32172  cvmlift3lem4  33184  msrrcl  33405  xpord2pred  33719  elmade  33978  brcolinear2  34287  topfneec  34471  bj-epelg  35166  cnpwstotbnd  35882  ismtyima  35888  ismndo2  35959  isrngo  35982  lshpkr  37058  elrfi  40432  climf  43053  climf2  43097  isupwlkg  45187