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

Theorem a1ii 25
Description: Add two antecedents to a wff. See a1iiALT 26 for a shorter proof using one more axiom. (Contributed by Jeff Hankins, 4-Aug-2009.) (Proof modification is discouraged.)
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 11 . 2  |-  ( ps 
->  ch )
32a1i 11 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ax12dgen3  1742  equviniOLD  2084  ax11f  2269  oaordi  6789  nnaordi  6861  map1  7185  cantnfval2  7624  infxpenc2lem1  7900  ackbij1lem16  8115  sornom  8157  fin23lem36  8228  isf32lem1  8233  isf32lem2  8234  zornn0g  8385  canthwe  8526  indpi  8784  uzindOLD  10364  seqid2  11369  fsum2d  12555  fsumabs  12580  fsumiun  12600  prmlem1a  13429  gicsubgen  15065  dis2ndc  17523  1stcelcls  17524  ptcmpfi  17845  caubl  19260  caublcls  19261  volsuplem  19449  cpnord  19821  fsumvma  20997  pntpbnd1  21280  incssnn0  26765  lzenom  26828  swrdccatin12lem4  28213  frgra3vlem1  28390  3vfriswmgralem  28394  iidn3  28583  truniALT  28626  onfrALTlem2  28632  ee220  28739  equviniNEW7  29527
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator