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

Theorem ancld 555
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 25 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 535 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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
This theorem is referenced by:  mo2v  2283  mopick2  2346  2eu6  2364  cgsexg  3056  cgsex2g  3057  cgsex4g  3058  reximdva0  3716  difsn  4077  preq12b  4119  elres  5102  relssres  5104  ordtr2  5429  elunirn  6115  fnoprabg  6355  tz7.49  7117  omord  7224  ficard  8941  fpwwe2lem12  9017  1idpr  9405  xrsupsslem  11543  xrinfmsslem  11544  fzospliti  11901  sqrt2irr  14244  algcvga  14481  prmind2  14578  infpn2  14800  grpinveu  16643  1stcrest  20410  fgss2  20831  fgcl  20835  filufint  20877  metrest  21481  reconnlem2  21787  plydivex  23192  ftalem3  23941  chtub  24082  2sqlem10  24244  dchrisum0flb  24290  pntpbnd1  24366  2pthfrgrarn2  25680  grpoidinvlem3  25876  grpoinveu  25892  ifbieq12d2  28105  elim2ifim  28108  iocinif  28313  tpr2rico  28670  bnj168  29490  dfon2lem8  30387  dftrpred3g  30425  nofulllem5  30544  nn0prpwlem  30927  voliunnfl  31891  dalem20  33170  elpaddn0  33277  cdleme25a  33832  cdleme29ex  33853  cdlemefr29exN  33881  dibglbN  34646  dihlsscpre  34714  lcfl7N  34981  mapdh9a  35270  mapdh9aOLDN  35271  hdmap11lem2  35325  ax6e2eq  36837
  Copyright terms: Public domain W3C validator