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

Theorem ancld 560
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 540 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  mo2v  2317  mopick2  2380  2eu6  2398  cgsexg  3092  cgsex2g  3093  cgsex4g  3094  reximdva0  3755  difsn  4119  preq12b  4164  elres  5159  relssres  5161  ordtr2  5486  elunirn  6181  fnoprabg  6424  tz7.49  7188  omord  7295  ficard  9016  fpwwe2lem12  9092  1idpr  9480  xrsupsslem  11621  xrinfmsslem  11622  fzospliti  11981  sqrt2irr  14350  algcvga  14587  prmind2  14684  infpn2  14906  grpinveu  16749  1stcrest  20517  fgss2  20938  fgcl  20942  filufint  20984  metrest  21588  reconnlem2  21894  plydivex  23299  ftalem3  24048  chtub  24189  2sqlem10  24351  dchrisum0flb  24397  pntpbnd1  24473  2pthfrgrarn2  25787  grpoidinvlem3  25983  grpoinveu  25999  ifbieq12d2  28208  elim2ifim  28211  iocinif  28412  tpr2rico  28767  bnj168  29587  dfon2lem8  30485  dftrpred3g  30523  nofulllem5  30644  nn0prpwlem  31027  voliunnfl  32029  dalem20  33303  elpaddn0  33410  cdleme25a  33965  cdleme29ex  33986  cdlemefr29exN  34014  dibglbN  34779  dihlsscpre  34847  lcfl7N  35114  mapdh9a  35403  mapdh9aOLDN  35404  hdmap11lem2  35458  ax6e2eq  36968
  Copyright terms: Public domain W3C validator