Theorem simp12r 1110

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp12r

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1023	. 2
2	1	3ad2ant1 1017	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  ackbij1lem16  8636  lsmcv  17787  nllyrest  19987  axcontlem4  24270  mzpcong  30910  eqlkr  34824  athgt  35180  llncvrlpln2  35281  4atlem11b  35332  2lnat  35508  cdlemblem  35517  pclfinN  35624  lhp2at0nle  35759  4atexlemex6  35798  cdlemd2  35924  cdlemd8  35930  cdleme15a  35999  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme20h  36042  cdleme21c  36053  cdleme21ct  36055  cdleme22cN  36068  cdleme23b  36076  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme32le  36173  cdleme35f  36180  cdlemf1  36287  trlord  36295  cdlemg7aN  36351  cdlemg33c0  36428  trlcone  36454  cdlemg44  36459  cdlemg48  36463  cdlemky  36652  cdlemk11ta  36655  cdleml4N  36705  dihmeetlem3N  37032  dihmeetlem13N  37046  mapdpglem32  37432  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439

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  df-an 371  df-3an 975