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

Step	Hyp	Ref	Expression
1		imim12d.1	. 2
2		imim12d.2	. . 3
3	2	imim2d 52	. 2
4	1, 3	syl5d 67	1

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