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  3895  rmob  3912  elpr2g  4673  oteqex  5519  epelg  5600  eqbrrdva  5894  relbrcnvg  6135  ordsucuniel  7860  ordsucun  7861  xpord2pred  8186  brtpos2  8273  eceqoveq  8880  elpmg  8901  elfi2  9483  brwdom  9636  brwdomn0  9638  rankr1c  9890  r1pwcl  9916  ttukeylem1  10578  fpwwe2lem8  10707  eltskm  10912  recmulnq  11033  clim  15540  rlim  15541  lo1o1  15578  o1lo1  15583  o1lo12  15584  rlimresb  15611  lo1eq  15614  rlimeq  15615  isercolllem2  15714  caucvgb  15728  saddisj  16511  sadadd  16513  sadass  16517  bitsshft  16521  smupvallem  16529  smumul  16539  catpropd  17767  isssc  17881  issubc  17899  funcres2b  17961  funcres2c  17968  sgrppropd  18769  mndpropd  18797  issubg3  19184  resghm2b  19274  resscntz  19373  elsymgbas  19415  odmulg  19598  dmdprd  20042  dprdw  20054  subgdmdprd  20078  lmodprop2d  20944  lssacs  20988  prmirred  21508  lindfmm  21870  lsslindf  21873  islinds3  21877  assapropd  21915  psrbaglefi  21969  cnrest2  23315  cnprest  23318  cnprest2  23319  lmss  23327  isfildlem  23886  isfcls  24038  elutop  24263  metustel  24584  blval2  24596  dscopn  24607  iscau2  25330  causs  25351  ismbf  25682  ismbfcn  25683  iblcnlem  25844  limcdif  25931  limcres  25941  limcun  25950  dvres  25966  q1peqb  26215  ulmval  26441  ulmres  26449  chpchtsum  27281  dchrisum0lem1  27578  elmade  27924  axcontlem5  29001  iswlkg  29649  issiga  34076  ismeas  34163  elcarsg  34270  cvmlift3lem4  35290  msrrcl  35511  brcolinear2  36022  topfneec  36321  bj-epelg  37034  cnpwstotbnd  37757  ismtyima  37763  ismndo2  37834  isrngo  37857  lshpkr  39073  fimgmcyc  42489  elrfi  42650  traxext  44910  climf  45543  climf2  45587  isupwlkg  47860