Theorem simplr1 1023

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

Assertion

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

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simpr1 987	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantr 462	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )

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

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 960

This theorem is referenced by:  soltmin  5225  frfi  7545  wemappo  7751  iccsplit  11405  ccatswrd  12334  sqrmo  12725  pcdvdstr  13925  vdwlem12  14036  mreexexlem4d  14568  iscatd2  14602  oppccomfpropd  14649  resssetc  14943  resscatc  14956  mod1ile  15258  mod2ile  15259  prdsmndd  15437  grprcan  15551  prdsrngd  16639  lmodprop2d  16931  lssintcl  16967  prdslmodd  16972  islmhm2  17041  islbs3  17158  ofco2  18174  mdetmul  18271  restopnb  18621  regsep2  18822  iuncon  18874  blsscls2  19921  met2ndci  19939  xrsblre  20230  colline  22918  f1otrg  22940  f1otrge  22941  ax5seglem4  23001  ax5seglem5  23002  axcontlem4  23036  axcontlem8  23040  axcontlem9  23041  axcontlem10  23042  eengtrkg  23054  submomnd  25997  ogrpaddltbi  26006  erdszelem8  26934  btwncomim  27891  btwnswapid  27895  broutsideof3  28004  outsideoftr  28007  outsidele  28010  mendassa  29396  subsubelfzo0  30056  el2wlksotot  30247  rusgranumwlks  30420  extwwlkfablem1  30513  lincresunit3lem2  30744  cvrletrN  32512  ltltncvr  32661  atcvrj2b  32670  2at0mat0  32763  paddasslem11  33068  pmod1i  33086  lautcvr  33330  tendoplass  34021  tendodi1  34022  tendodi2  34023  cdlemk34  34148