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  1713  equvini  1940  ax11f  2144  oaordi  6560  nnaordi  6632  map1  6955  cantnfval2  7386  infxpenc2lem1  7662  ackbij1lem16  7877  sornom  7919  fin23lem36  7990  isf32lem1  7995  isf32lem2  7996  zornn0g  8148  canthwe  8289  indpi  8547  uzindOLD  10122  seqid2  11108  fsum2d  12250  fsumabs  12275  fsumiun  12295  prmlem1a  13124  gicsubgen  14758  dis2ndc  17202  1stcelcls  17203  ptcmpfi  17520  caubl  18749  caublcls  18750  volsuplem  18928  cpnord  19300  fsumvma  20468  pntpbnd1  20751  eqfnung2  25221  dupre1  25346  isconcl5a  26204  isconcl5ab  26205  nbssntrs  26250  incssnn0  26889  lzenom  26952  frgra3vlem1  28424  3vfriswmgralem  28428  iidn3  28561  truniALT  28604  onfrALTlem2  28610  ee220  28715  equviniNEW7  29502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator