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

Theorem ancld 537
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
Hypothesis
Ref Expression
ancld.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ancld  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )

Proof of Theorem ancld
StepHypRef Expression
1 idd 22 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 520 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mopick2  2307  cgsexg  2932  cgsex2g  2933  cgsex4g  2934  reximdva0  3584  difsn  3878  preq12b  3918  ordtr2  4568  elres  5123  relssres  5125  elunirnALT  5941  fnoprabg  6112  tz7.49  6640  omord  6749  ficard  8375  fpwwe2lem12  8451  1idpr  8841  xrsupsslem  10819  xrinfmsslem  10820  fzospliti  11097  sqr2irr  12777  algcvga  12999  prmind2  13019  infpn2  13210  grpinveu  14768  1stcrest  17439  fgss2  17829  fgcl  17833  filufint  17875  metrest  18446  reconnlem2  18731  plydivex  20083  ftalem3  20726  chtub  20865  2sqlem10  21027  dchrisum0flb  21073  pntpbnd1  21149  grpoidinvlem3  21644  grpoinveu  21660  ifbieq12d2  23848  elim2ifim  23852  iocinif  23982  tpr2rico  24116  dfon2lem8  25172  dftrpred3g  25262  nofulllem5  25386  voliunnfl  25957  nn0prpwlem  26018  2pthfrgrarn2  27765  a9e2eq  27989  bnj168  28437  dalem20  29809  elpaddn0  29916  cdleme25a  30469  cdleme29ex  30490  cdlemefr29exN  30518  dibglbN  31283  dihlsscpre  31351  lcfl7N  31618  mapdh9a  31907  mapdh9aOLDN  31908  hdmap11lem2  31962
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
  Copyright terms: Public domain W3C validator