Theorem pm5.21ndd 354

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 133	. . 3
4		pm5.21ndd.2	. . . 4
5	4	con3d 133	. . 3
6		pm5.21im 349	. . 3
7	3, 5, 6	syl6c 64	. 2
8	1, 7	pm2.61d 158	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184

This theorem is referenced by:  pm5.21nd  900  rmob  3430  oteqex  4745  epelg  4797  eqbrrdva  5177  relbrcnvg  5380  ordsucuniel  6659  ordsucun  6660  brtpos2  6980  eceqoveq  7435  elpmg  7454  elfi2  7894  brwdom  8014  brwdomn0  8016  rankr1c  8260  r1pwcl  8286  ttukeylem1  8910  fpwwe2lem9  9037  eltskm  9242  recmulnq  9363  clim  13317  rlim  13318  lo1o1  13355  o1lo1  13360  o1lo12  13361  rlimresb  13388  lo1eq  13391  rlimeq  13392  isercolllem2  13488  caucvgb  13502  saddisj  14115  sadadd  14117  sadass  14121  bitsshft  14125  smupvallem  14133  smumul  14143  catpropd  15104  isssc  15189  issubc  15204  funcres2b  15266  funcres2c  15270  mndpropd  15946  issubg3  16219  resghm2b  16285  resscntz  16369  elsymgbas  16407  odmulg  16578  dmdprd  17029  dprdw  17043  dprdwOLD  17050  subgdmdprd  17081  lmodprop2d  17572  lssacs  17613  assapropd  17976  psrbaglefi  18023  psrbaglefiOLD  18024  prmirred  18525  prmirredOLD  18528  lindfmm  18862  lsslindf  18865  islinds3  18869  cnrest2  19787  cnprest  19790  cnprest2  19791  lmss  19799  isfildlem  20358  isfcls  20510  elutop  20736  metustelOLD  21054  metustel  21055  blval2  21078  dscopn  21094  iscau2  21716  causs  21737  ismbf  22037  ismbfcn  22038  iblcnlem  22195  limcdif  22280  limcres  22290  limcun  22299  dvres  22315  q1peqb  22555  ulmval  22775  ulmres  22783  chpchtsum  23494  dchrisum0lem1  23701  axcontlem5  24271  iseupa  24965  ismndo2  25347  isrngo  25380  issiga  28111  ismeas  28170  cvmlift3lem4  28767  msrrcl  28903  brcolinear2  29708  topfneec  30173  cnpwstotbnd  30293  ismtyima  30299  elrfi  30626  climf  31628  lshpkr  34842

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 185