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

Theorem a1ii 24
Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypothesis
Ref Expression
a1ii.1  |-  ch
Assertion
Ref Expression
a1ii  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem a1ii
StepHypRef Expression
1 a1ii.1 . . 3  |-  ch
21a1i 10 . 2  |-  ( ph  ->  ch )
32a1d 22 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ax12dgen3  1701  equvini  1927  ax11f  2131  oaordi  6544  nnaordi  6616  map1  6939  cantnfval2  7370  infxpenc2lem1  7646  ackbij1lem16  7861  sornom  7903  fin23lem36  7974  isf32lem1  7979  isf32lem2  7980  zornn0g  8132  canthwe  8273  indpi  8531  uzindOLD  10106  seqid2  11092  fsum2d  12234  fsumabs  12259  fsumiun  12279  prmlem1a  13108  gicsubgen  14742  dis2ndc  17186  1stcelcls  17187  ptcmpfi  17504  caubl  18733  caublcls  18734  volsuplem  18912  cpnord  19284  fsumvma  20452  pntpbnd1  20735  eqfnung2  25118  dupre1  25243  isconcl5a  26101  isconcl5ab  26102  nbssntrs  26147  incssnn0  26786  lzenom  26849  frgra3vlem1  28178  3vfriswmgralem  28182  iidn3  28262  truniALT  28305  onfrALTlem2  28311  ee220  28410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator