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  2165  sbcrext  3652  sbcrextOLD  3653  oaordi  7795  nnaordi  7867  map1  8201  cantnfval2  8739  infxpenc2lem1  9032  ackbij1lem16  9249  sornom  9291  fin23lem36  9362  isf32lem1  9367  isf32lem2  9368  zornn0g  9519  canthwe  9665  indpi  9921  seqid2  13041  swrdccatin12lem3  13690  fsum2d  14701  fsumabs  14732  fsumiun  14752  fprod2d  14910  prmodvdslcmf  15953  prmlem1a  16015  gicsubgen  17921  dmatelnd  20504  dis2ndc  21465  1stcelcls  21466  ptcmpfi  21818  caubl  23306  caublcls  23307  volsuplem  23523  cpnord  23897  fsumvma  25137  gausslemma2dlem4  25293  pntpbnd1  25474  clwwlknonex2lem2  27257  3pthdlem1  27316  frgr3vlem1  27427  3vfriswmgrlem  27431  fzto1st  30162  psgnfzto1st  30164  wl-equsal1t  33640  ax12f  34729  incssnn0  37776  lzenom  37835  clsk1independent  38846  iidn3  39209  truniALT  39253  onfrALTlem2  39263  ee220  39365  dvmptfprodlem  40662  fourierdlem89  40915  fourierdlem91  40917  sge0reuz  41167  hoi2toco  41327  linds0  42764
 Copyright terms: Public domain W3C validator