Theorem simp1rl 1126

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

Assertion

Ref	Expression
simp1rl	|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ph )

Proof of Theorem simp1rl

Step	Hyp	Ref	Expression
1		simprl 794	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1imass  6521  smo11  7461  zsupss  11777  lsmcv  19141  lspsolvlem  19142  mat2pmatghm  20535  mat2pmatmul  20536  plyadd  23973  plymul  23974  coeeu  23981  aannenlem1  24083  logexprlim  24950  ax5seglem6  25814  ax5seg  25818  mdetpmtr1  29889  mdetpmtr2  29890  wsuclem  31773  wsuclemOLD  31774  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem12  32205  lshpsmreu  34396  2llnmat  34810  lvolex3N  34824  lnjatN  35066  pclfinclN  35236  lhpat3  35332  cdlemd6  35490  cdlemfnid  35852  cdlemk19ylem  36218  dihlsscpre  36523  dih1dimb2  36530  dihglblem6  36629  pellex  37399  mullimc  39848  mullimcf  39855  limcperiod  39860  cncfshift  40087  cncfperiod  40092