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

Theorem a1ii 26
Description: Add two antecedents to a wff. See a1iiALT 27 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  1743  equviniOLD  2085  ax11f  2271  oaordi  6792  nnaordi  6864  map1  7188  cantnfval2  7627  infxpenc2lem1  7905  ackbij1lem16  8120  sornom  8162  fin23lem36  8233  isf32lem1  8238  isf32lem2  8239  zornn0g  8390  canthwe  8531  indpi  8789  uzindOLD  10369  seqid2  11374  fsum2d  12560  fsumabs  12585  fsumiun  12605  prmlem1a  13434  gicsubgen  15070  dis2ndc  17528  1stcelcls  17529  ptcmpfi  17850  caubl  19265  caublcls  19266  volsuplem  19454  cpnord  19826  fsumvma  21002  pntpbnd1  21285  incssnn0  26779  lzenom  26842  swrdccatin12lem4  28247  frgra3vlem1  28464  3vfriswmgralem  28468  iidn3  28657  truniALT  28700  onfrALTlem2  28706  ee220  28813  equviniNEW7  29601
This theorem was proved from axioms:  ax-mp 5  ax-1 6
  Copyright terms: Public domain W3C validator