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

Theorem simpll3 999
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 963 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 453 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ordiso2  7513  wemappo  7547  iunfictbso  8026  fin1a2lem12  8322  fin1a2lem13  8323  prlem934  8941  ifle  10814  xlesubadd  10873  icoshftf1o  11051  swrdcl  11797  subcn2  12419  rpdvds  13155  qexpz  13301  ramval  13407  0ram  13419  mreexexd  13904  gsumccat  14818  odmulg  15223  pgpfi1  15260  lsmcl  16186  lbsextlem3  16263  coe1mul2  16693  iscnp4  17358  cnpnei  17359  cnconst2  17378  cnpdis  17388  cnhaus  17449  ordthauslem  17478  clscon  17524  nlly2i  17570  txcn  17689  ordthmeolem  17864  flimrest  18046  isfcf  18097  alexsubALTlem4  18112  ghmcnp  18175  utop2nei  18311  blssps  18485  blss  18486  metcnp3  18601  metcnp  18602  xrsxmet  18871  metdseq0  18915  xrhmeo  19002  cfil3i  19253  caucfil  19267  cfilres  19280  fta1b  20123  mumul  20995  lgsfcl2  21117  lgsdir  21145  lgsne0  21148  pjhthmo  22835  xrge0adddir  24246  probun  24708  cnpcon  24948  axbtwnid  25909  axcontlem2  25935  axcontlem4  25937  axcontlem7  25940  axcontlem8  25941  outsideofeq  26095  linethru  26118  nacsfix  26804  mzpsubst  26843  diophrw  26855  lzunuz  26864  jm2.19  27102  jm2.27  27117  islindf4  27323  hbtlem5  27347  pmtrf  27412  rfcnnnub  27721  stoweidlem20  27783  stoweidlem61  27824  elfzonelfzo  28179  atlatmstc  30215  cvlcvr1  30235  ishlat3N  30250  hlrelat  30297  intnatN  30302  cvrval5  30310  atcvrlln  30415  llnexatN  30416  2at0mat0  30420  llncvrlpln  30453  lplnexllnN  30459  lplncvrlvol  30511  lncvrelatN  30676  pmapjoin  30747  pmapjat1  30748  pclclN  30786  osumclN  30862  lhprelat3N  30935  cdlemd5  31097  cdleme32fvcl  31335  cdlemg39  31611  ltrncom  31633  dihmeetALTN  32223  dochss  32261  mapdrvallem2  32541
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator