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  1784  ax12f  2263  sbcrext  3414  oaordi  7196  nnaordi  7268  map1  7595  cantnfval2  8089  cantnfval2OLD  8119  infxpenc2lem1  8397  ackbij1lem16  8616  sornom  8658  fin23lem36  8729  isf32lem1  8734  isf32lem2  8735  zornn0g  8886  canthwe  9030  indpi  9286  uzindOLD  10956  seqid2  12122  swrdccatin12lem3  12681  fsum2d  13552  fsumabs  13581  fsumiun  13601  prmlem1a  14453  gicsubgen  16140  dmatelnd  18805  dis2ndc  19767  1stcelcls  19768  ptcmpfi  20141  caubl  21573  caublcls  21574  volsuplem  21792  cpnord  22165  fsumvma  23313  pntpbnd1  23596  frgra3vlem1  24773  3vfriswmgralem  24777  wl-equsal1t  29847  incssnn0  30474  lzenom  30534  lptioo2  31400  lptioo1  31401  ioodvbdlimc1lem1  31488  fourierdlem45  31679  fourierdlem89  31723  fourierdlem91  31725  linds0  32364  iidn3  32566  truniALT  32609  onfrALTlem2  32615  ee220  32721
  Copyright terms: Public domain W3C validator