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

Theorem simpll3 1029
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 993 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ordiso2  7841  wemappo  7875  iunfictbso  8396  fin1a2lem12  8692  fin1a2lem13  8693  prlem934  9314  ifle  11279  xlesubadd  11338  icoshftf1o  11526  elfzonelfzo  11745  swrdcl  12434  repswccat  12542  subcn2  13191  rpdvds  13929  qexpz  14082  ramval  14188  0ram  14200  cshwrepswhash1  14248  mreexexd  14706  gsumccat  15639  gsmsymgreqlem1  16055  pmtrf  16081  odmulg  16179  pgpfi1  16216  lsmcl  17288  lbsextlem3  17365  coe1mul2  17847  islindf4  18393  cramerlem2  18627  iscnp4  19000  cnpnei  19001  cnconst2  19020  cnpdis  19030  cnhaus  19091  ordthauslem  19120  clscon  19167  nlly2i  19213  txcn  19332  ordthmeolem  19507  flimrest  19689  isfcf  19740  alexsubALTlem4  19755  ghmcnp  19818  utop2nei  19958  blssps  20132  blss  20133  metcnp3  20248  metcnp  20249  xrsxmet  20519  metdseq0  20563  xrhmeo  20651  cfil3i  20913  caucfil  20927  cfilres  20940  fta1b  21775  mumul  22653  lgsfcl2  22775  lgsdir  22803  lgsne0  22806  istrkgcb  23051  axbtwnid  23338  axcontlem2  23364  axcontlem4  23366  axcontlem7  23369  axcontlem8  23370  pjhthmo  24858  xrge0adddir  26301  archiabl  26361  probun  26947  cnpcon  27264  outsideofeq  28306  linethru  28329  nacsfix  29197  mzpsubst  29234  diophrw  29246  lzunuz  29255  jm2.19  29491  jm2.27  29506  hbtlem5  29633  rfcnnnub  29907  stoweidlem20  29964  stoweidlem61  30005  rmsupp0  30930  rmsuppss  30932  fsuppmapnn0fiub0  30950  cpmadugsumlemF  31363  cayhamlem4  31376  atlatmstc  33303  cvlcvr1  33323  ishlat3N  33338  hlrelat  33385  intnatN  33390  cvrval5  33398  atcvrlln  33503  llnexatN  33504  2at0mat0  33508  llncvrlpln  33541  lplnexllnN  33547  lplncvrlvol  33599  lncvrelatN  33764  pmapjoin  33835  pmapjat1  33836  pclclN  33874  osumclN  33950  lhprelat3N  34023  cdlemd5  34185  cdleme32fvcl  34423  cdlemg39  34699  ltrncom  34721  dihmeetALTN  35311  dochss  35349  mapdrvallem2  35629
  Copyright terms: Public domain W3C validator