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

Theorem ancld 551
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 24 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 531 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  mo2v  2291  mo2vOLD  2292  mo2vOLDOLD  2293  mopick2  2359  2eu6  2380  cgsexg  3139  cgsex2g  3140  cgsex4g  3141  reximdva0  3795  difsn  4150  preq12b  4192  ordtr2  4911  elres  5297  relssres  5299  elunirn  6138  fnoprabg  6376  tz7.49  7102  omord  7209  ficard  8931  fpwwe2lem12  9008  1idpr  9396  xrsupsslem  11501  xrinfmsslem  11502  fzospliti  11834  sqrt2irr  14066  algcvga  14292  prmind2  14312  infpn2  14515  grpinveu  16283  1stcrest  20120  fgss2  20541  fgcl  20545  filufint  20587  metrest  21193  reconnlem2  21498  plydivex  22859  ftalem3  23546  chtub  23685  2sqlem10  23847  dchrisum0flb  23893  pntpbnd1  23969  2pthfrgrarn2  25212  grpoidinvlem3  25406  grpoinveu  25422  ifbieq12d2  27626  elim2ifim  27629  iocinif  27826  tpr2rico  28129  dfon2lem8  29462  dftrpred3g  29556  nofulllem5  29706  voliunnfl  30298  nn0prpwlem  30380  ax6e2eq  33724  bnj168  34186  dalem20  35814  elpaddn0  35921  cdleme25a  36476  cdleme29ex  36497  cdlemefr29exN  36525  dibglbN  37290  dihlsscpre  37358  lcfl7N  37625  mapdh9a  37914  mapdh9aOLDN  37915  hdmap11lem2  37969
  Copyright terms: Public domain W3C validator