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  3823  rmob  3840  elpr2g  4606  oteqex  5448  epelg  5525  eqbrrdva  5818  relbrcnvg  6064  ordsucuniel  7766  ordsucun  7767  xpord2pred  8087  brtpos2  8174  eceqoveq  8759  elpmg  8780  elfi2  9317  brwdom  9472  brwdomn0  9474  rankr1c  9733  r1pwcl  9759  ttukeylem1  10419  fpwwe2lem8  10549  eltskm  10754  recmulnq  10875  clim  15417  rlim  15418  lo1o1  15455  o1lo1  15460  o1lo12  15461  rlimresb  15488  lo1eq  15491  rlimeq  15492  isercolllem2  15589  caucvgb  15603  saddisj  16392  sadadd  16394  sadass  16398  bitsshft  16402  smupvallem  16410  smumul  16420  catpropd  17632  isssc  17744  issubc  17759  funcres2b  17821  funcres2c  17827  sgrppropd  18656  mndpropd  18684  issubg3  19074  resghm2b  19163  resscntz  19262  elsymgbas  19303  odmulg  19485  dmdprd  19929  dprdw  19941  subgdmdprd  19965  lmodprop2d  20875  lssacs  20918  prmirred  21429  lindfmm  21782  lsslindf  21785  islinds3  21789  assapropd  21827  psrbaglefi  21882  cnrest2  23230  cnprest  23233  cnprest2  23234  lmss  23242  isfildlem  23801  isfcls  23953  elutop  24177  metustel  24494  blval2  24506  dscopn  24517  iscau2  25233  causs  25254  ismbf  25585  ismbfcn  25586  iblcnlem  25746  limcdif  25833  limcres  25843  limcun  25852  dvres  25868  q1peqb  26117  ulmval  26345  ulmres  26353  chpchtsum  27186  dchrisum0lem1  27483  elmade  27853  axcontlem5  29041  iswlkg  29687  issiga  34269  ismeas  34356  elcarsg  34462  cvmlift3lem4  35516  msrrcl  35737  brcolinear2  36252  topfneec  36549  bj-epelg  37269  cnpwstotbnd  37994  ismtyima  38000  ismndo2  38071  isrngo  38094  lshpkr  39373  fimgmcyc  42785  elrfi  42932  traxext  45214  climf  45864  climf2  45906  isupwlkg  48379