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  3848  rmob  3865  elpr2g  4627  oteqex  5475  epelg  5554  eqbrrdva  5849  relbrcnvg  6092  ordsucuniel  7816  ordsucun  7817  xpord2pred  8142  brtpos2  8229  eceqoveq  8834  elpmg  8855  elfi2  9424  brwdom  9579  brwdomn0  9581  rankr1c  9833  r1pwcl  9859  ttukeylem1  10521  fpwwe2lem8  10650  eltskm  10855  recmulnq  10976  clim  15508  rlim  15509  lo1o1  15546  o1lo1  15551  o1lo12  15552  rlimresb  15579  lo1eq  15582  rlimeq  15583  isercolllem2  15680  caucvgb  15694  saddisj  16482  sadadd  16484  sadass  16488  bitsshft  16492  smupvallem  16500  smumul  16510  catpropd  17719  isssc  17831  issubc  17846  funcres2b  17908  funcres2c  17914  sgrppropd  18707  mndpropd  18735  issubg3  19125  resghm2b  19215  resscntz  19314  elsymgbas  19353  odmulg  19535  dmdprd  19979  dprdw  19991  subgdmdprd  20015  lmodprop2d  20879  lssacs  20922  prmirred  21433  lindfmm  21785  lsslindf  21788  islinds3  21792  assapropd  21830  psrbaglefi  21884  cnrest2  23222  cnprest  23225  cnprest2  23226  lmss  23234  isfildlem  23793  isfcls  23945  elutop  24170  metustel  24487  blval2  24499  dscopn  24510  iscau2  25227  causs  25248  ismbf  25579  ismbfcn  25580  iblcnlem  25740  limcdif  25827  limcres  25837  limcun  25846  dvres  25862  q1peqb  26111  ulmval  26339  ulmres  26347  chpchtsum  27180  dchrisum0lem1  27477  elmade  27823  axcontlem5  28893  iswlkg  29539  issiga  34089  ismeas  34176  elcarsg  34283  cvmlift3lem4  35290  msrrcl  35511  brcolinear2  36022  topfneec  36319  bj-epelg  37032  cnpwstotbnd  37767  ismtyima  37773  ismndo2  37844  isrngo  37867  lshpkr  39081  fimgmcyc  42504  elrfi  42664  traxext  44950  climf  45599  climf2  45643  isupwlkg  48060