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

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

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 962 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ordiso2  7473  wemappo  7507  iunfictbso  7984  fin1a2lem12  8280  fin1a2lem13  8281  prlem934  8899  ifle  10772  xlesubadd  10831  icoshftf1o  11009  swrdcl  11754  subcn2  12376  rpdvds  13112  qexpz  13258  ramval  13364  0ram  13376  mreexexd  13861  gsumccat  14775  odmulg  15180  pgpfi1  15217  lsmcl  16143  lbsextlem3  16220  coe1mul2  16650  iscnp4  17315  cnpnei  17316  cnconst2  17335  cnpdis  17345  cnhaus  17406  ordthauslem  17435  clscon  17481  nlly2i  17527  txcn  17646  ordthmeolem  17821  flimrest  18003  isfcf  18054  alexsubALTlem4  18069  ghmcnp  18132  utop2nei  18268  blssps  18442  blss  18443  metcnp3  18558  metcnp  18559  xrsxmet  18828  metdseq0  18872  xrhmeo  18959  cfil3i  19210  caucfil  19224  cfilres  19237  fta1b  20080  mumul  20952  lgsfcl2  21074  lgsdir  21102  lgsne0  21105  pjhthmo  22792  xrge0adddir  24203  probun  24665  cnpcon  24905  axbtwnid  25826  axcontlem2  25852  axcontlem4  25854  axcontlem7  25857  axcontlem8  25858  outsideofeq  26012  linethru  26035  nacsfix  26703  mzpsubst  26742  diophrw  26754  lzunuz  26763  jm2.19  27001  jm2.27  27016  islindf4  27223  hbtlem5  27247  pmtrf  27312  rfcnnnub  27621  stoweidlem20  27683  stoweidlem61  27724  elfzonelfzo  28044  swrdccatin12lem3  28099  atlatmstc  29956  cvlcvr1  29976  ishlat3N  29991  hlrelat  30038  intnatN  30043  cvrval5  30051  atcvrlln  30156  llnexatN  30157  2at0mat0  30161  llncvrlpln  30194  lplnexllnN  30200  lplncvrlvol  30252  lncvrelatN  30417  pmapjoin  30488  pmapjat1  30489  pclclN  30527  osumclN  30603  lhprelat3N  30676  cdlemd5  30838  cdleme32fvcl  31076  cdlemg39  31352  ltrncom  31374  dihmeetALTN  31964  dochss  32002  mapdrvallem2  32282
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator