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  2141  sbcrext  3805  oaordi  8159  nnaordi  8231  mapsnend  8575  cantnfval2  9120  infxpenc2lem1  9434  ackbij1lem16  9650  sornom  9692  fin23lem36  9763  isf32lem1  9768  isf32lem2  9769  zornn0g  9920  canthwe  10066  indpi  10322  seqid2  13416  pfxccatin12lem3  14089  fsum2d  15122  fsumabs  15152  fsumiun  15172  fprod2d  15331  prmodvdslcmf  16377  prmlem1a  16436  gicsubgen  18414  dmatelnd  21105  dis2ndc  22069  1stcelcls  22070  ptcmpfi  22422  caubl  23916  caublcls  23917  volsuplem  24163  cpnord  24542  fsumvma  25801  gausslemma2dlem4  25957  pntpbnd1  26174  3pthdlem1  27953  frgr3vlem1  28062  3vfriswmgrlem  28066  fzto1st  30799  psgnfzto1st  30801  wl-equsal1t  34945  ax12f  36235  incssnn0  39645  lzenom  39704  clsk1independent  40742  iidn3  41200  truniALT  41240  onfrALTlem2  41245  ee220  41337  dvmptfprodlem  42579  fourierdlem89  42830  fourierdlem91  42832  sge0reuz  43079  hoi2toco  43239  linds0  44867
 Copyright terms: Public domain W3C validator