MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1ii 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
Assertion
Ref Expression
a1ii

Proof of Theorem a1ii
StepHypRef Expression
1 a1ii.1 . . 3
21a1i 11 . 2
32a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  ax13dgen3  1835  ax12f  2270  sbcrext  3410  oaordi  7214  nnaordi  7286  map1  7614  cantnfval2  8109  cantnfval2OLD  8139  infxpenc2lem1  8417  ackbij1lem16  8636  sornom  8678  fin23lem36  8749  isf32lem1  8754  isf32lem2  8755  zornn0g  8906  canthwe  9050  indpi  9306  uzindOLD  10982  seqid2  12153  swrdccatin12lem3  12715  fsum2d  13586  fsumabs  13615  fsumiun  13635  fprod2d  13785  prmlem1a  14592  gicsubgen  16326  dmatelnd  18998  dis2ndc  19961  1stcelcls  19962  ptcmpfi  20314  caubl  21746  caublcls  21747  volsuplem  21965  cpnord  22338  fsumvma  23488  pntpbnd1  23771  frgra3vlem1  25000  3vfriswmgralem  25004  wl-equsal1t  29994  incssnn0  30643  lzenom  30703  dvmptfprodlem  31741  fourierdlem89  31978  fourierdlem91  31980  linds0  33066  iidn3  33270  truniALT  33312  onfrALTlem2  33318  ee220  33424
This theorem was proved from axioms:  ax-mp 5  ax-1 6
  Copyright terms: Public domain W3C validator