Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim12d Unicode version

Theorem imim12d 74
 Description: Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.)
Hypotheses
Ref Expression
imim12d.1
imim12d.2
Assertion
Ref Expression
imim12d

Proof of Theorem imim12d
StepHypRef Expression
1 imim12d.1 . 2
2 imim12d.2 . . 3
32imim2d 52 . 2
41, 3syl5d 67 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4 This theorem is referenced by:  imim1d  75  mo3OLD  2324  rspcimdv  3211  peano5  6723  isf34lem6  8781  inar1  9174  supsrlem  9509  uzindOLD  10982  r19.29uz  13183  o1of2  13435  o1rlimmul  13441  caucvg  13501  isprm5  14253  mrissmrid  15038  kgen2ss  20056  txlm  20149  isr0  20238  metcnpi3  21049  addcnlem  21368  nmhmcn  21603  aalioulem5  22732  xrlimcnp  23298  dmdmd  27219  mdsl0  27229  mdsl1i  27240  xrge0infss  27580  lmxrge0  27934  ghomf1olem  29034  ax8dfeq  29231  heicant  30049  ispridlc  30467  infrglb  31584  bnj517  33943 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
 Copyright terms: Public domain W3C validator