MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl3l Structured version   Unicode version

Theorem simpl3l 1060
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl3l  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )

Proof of Theorem simpl3l
StepHypRef Expression
1 simp3l 1033 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 466 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  tfisi  6700  omopth2  7297  ltmul1a  10462  xaddass  11543  xlemul2a  11583  swrdsbslen  12807  dvdsadd2b  14347  pockthg  14850  psgnunilem4  17138  efgred  17398  ptbasin  20591  basqtop  20725  xrsmopn  21829  axpasch  24970  axcontlem4  24996  br4  30406  btwnintr  30792  btwnexch3  30793  btwnouttr2  30795  cgrxfr  30828  lineext  30849  btwnconn1lem13  30872  btwnconn1lem14  30873  btwnconn3  30876  brsegle  30881  brsegle2  30882  segleantisym  30888  outsideofeu  30904  lineunray  30920  lineelsb2  30921  cvrcmp  32819  atcvrj2b  32967  3dimlem3  32996  3dimlem3OLDN  32997  3dim3  33004  ps-1  33012  lplnnle2at  33076  2llnm3N  33104  lvolnle3at  33117  4atlem0a  33128  4atlem3  33131  4atlem3a  33132  lnatexN  33314  paddasslem8  33362  paddasslem9  33363  paddasslem10  33364  paddasslem12  33366  paddasslem13  33367  lhp2lt  33536  lhpexle2lem  33544  lhpexle3  33547  lhpmcvr3  33560  lhpat3  33581  4atex  33611  trlval2  33699  ltrnideq  33711  ltrnatlw  33719  trlnle  33722  trlval4  33724  cdlemd4  33737  cdlemd5  33738  cdleme16  33821  cdleme21  33874  cdleme21k  33875  cdleme27cl  33903  cdleme27N  33906  cdleme29ex  33911  cdleme43fsv1snlem  33957  cdleme40m  34004  cdleme46f2g2  34030  cdleme46f2g1  34031  trlord  34106  cdlemg8  34168  cdlemg15a  34192  cdlemg16z  34196  cdlemg18a  34215  cdlemg24  34225  cdlemg38  34252  cdlemg40  34254  trlcone  34265  cdlemj2  34359  tendoid0  34362  tendoconid  34366  cdlemk34  34447  cdlemk38  34452  cdlemkid4  34471  cdlemk35s-id  34475  cdlemk39s-id  34477  cdlemk53  34494  tendospcanN  34561  cdlemm10N  34656  dihvalcqpre  34773  dihopelvalcpre  34786  dihord5b  34797  dihglblem5apreN  34829  dihmeetlem16N  34860  dihmeetlem17N  34861  dvh3dim3N  34987  qirropth  35727  mzpcong  35793  jm2.26  35828  aomclem6  35888  limcleqr  37666  fourierdlem42  37953  fourierdlem42OLD  37954
  Copyright terms: Public domain W3C validator