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

Theorem a1ii 27
Description: Add two antecedents to a wff. (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 setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6
This theorem is referenced by:  ax13dgen3  1773  ax12f  2241  sbcrext  3281  oaordi  6997  nnaordi  7069  map1  7400  cantnfval2  7889  cantnfval2OLD  7919  infxpenc2lem1  8197  ackbij1lem16  8416  sornom  8458  fin23lem36  8529  isf32lem1  8534  isf32lem2  8535  zornn0g  8686  canthwe  8830  indpi  9088  uzindOLD  10748  seqid2  11864  swrdccatin12lem3  12393  fsum2d  13250  fsumabs  13276  fsumiun  13296  prmlem1a  14146  gicsubgen  15818  dis2ndc  19076  1stcelcls  19077  ptcmpfi  19398  caubl  20830  caublcls  20831  volsuplem  21048  cpnord  21421  fsumvma  22564  pntpbnd1  22847  wl-equsal1t  28382  incssnn0  29059  lzenom  29120  frgra3vlem1  30604  3vfriswmgralem  30608  dmatelnd  30887  linds0  31011  iidn3  31217  truniALT  31260  onfrALTlem2  31266  ee220  31372
  Copyright terms: Public domain W3C validator