MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2a1i Structured version   Visualization version   GIF 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 𝜑
Assertion
Ref Expression
2a1i (𝜓 → (𝜒𝜑))

Proof of Theorem 2a1i
StepHypRef Expression
1 2a1i.1 . . 3 𝜑
21a1i 11 . 2 (𝜒𝜑)
32a1i 11 1 (𝜓 → (𝜒𝜑))
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  2127  sbcrext  3863  mptexgf  7234  oaordi  8567  nnaordi  8639  mapsnend  9061  cantnfval2  9694  infxpenc2lem1  10044  ackbij1lem16  10260  sornom  10302  fin23lem36  10373  isf32lem1  10378  isf32lem2  10379  zornn0g  10530  canthwe  10676  indpi  10932  seqid2  14049  pfxccatin12lem3  14718  fsum2d  15753  fsumabs  15783  fsumiun  15803  fprod2d  15961  prmodvdslcmf  17019  prmlem1a  17079  gicsubgen  19242  dmatelnd  22442  dis2ndc  23408  1stcelcls  23409  ptcmpfi  23761  caubl  25280  caublcls  25281  volsuplem  25528  cpnord  25909  fsumvma  27191  gausslemma2dlem4  27347  pntpbnd1  27564  3pthdlem1  30046  frgr3vlem1  30155  3vfriswmgrlem  30159  fzto1st  32916  psgnfzto1st  32918  wl-equsal1t  37140  ax12f  38542  incssnn0  42273  lzenom  42332  omabs2  42903  clsk1independent  43618  iidn3  44082  truniALT  44122  onfrALTlem2  44127  ee220  44219  dvmptfprodlem  45470  fourierdlem89  45721  fourierdlem91  45723  sge0reuz  45973  hoi2toco  46133  linds0  47719
  Copyright terms: Public domain W3C validator