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

Theorem 2a1i 12
Description: Inference introducing two antecedents. Two applications of a1i 11. Inference associated with 2a1 28. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypothesis
Ref Expression
2a1i.1  |-  ph
Assertion
Ref Expression
2a1i  |-  ( ps 
->  ( ch  ->  ph )
)

Proof of Theorem 2a1i
StepHypRef Expression
1 2a1i.1 . . 3  |-  ph
21a1i 11 . 2  |-  ( ch 
->  ph )
32a1i 11 1  |-  ( ps 
->  ( ch  ->  ph )
)
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  1923  sbcrext  3352  oaordi  7272  nnaordi  7344  map1  7673  cantnfval2  8199  infxpenc2lem1  8475  ackbij1lem16  8690  sornom  8732  fin23lem36  8803  isf32lem1  8808  isf32lem2  8809  zornn0g  8960  canthwe  9101  indpi  9357  seqid2  12290  swrdccatin12lem3  12882  fsum2d  13880  fsumabs  13909  fsumiun  13929  fprod2d  14083  prmodvdslcmf  15053  prmordvdslcmfOLD  15067  prmlem1a  15126  gicsubgen  16990  dmatelnd  19569  dis2ndc  20523  1stcelcls  20524  ptcmpfi  20876  caubl  22325  caublcls  22326  volsuplem  22556  cpnord  22937  fsumvma  24189  pntpbnd1  24472  frgra3vlem1  25776  3vfriswmgralem  25780  fzto1st  28664  psgnfzto1st  28666  wl-equsal1t  31918  ax12f  32555  incssnn0  35597  lzenom  35656  iidn3  36900  truniALT  36945  onfrALTlem2  36955  ee220  37059  dvmptfprodlem  37856  fourierdlem89  38096  fourierdlem91  38098  hoi2toco  38466  3pthdlem1  39904  linds0  40530
  Copyright terms: Public domain W3C validator